PR summary 962b24680e

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

Should this be abbrevs? Do we want to go through and refactor the Valued files to use these?

I think they should be defs, just like the Metric variants.

Do these naturally carry algebraic structures that we should define right away? Are they subrings?

The open and closed balls are closed under addition, but if the radius is too big they are not closed under multiplication. So I guess they can be of type AddSubgroup R instead of Set R.

Moreover, they could be a Submodule v.integer R. But then it would have to be defined in Ringtheory/Valuation/Integers.lean

We already have https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Valuation/Basic.html#Valuation.ltAddSubgroup, and in #26829, I define the le, ideal, and submodule versions.

Interesting. Then I would think that ltSubmodule/leSubmodule can be used instead of ball/closedBall. Maybe then ltSubmodule/leSubmodule could be renamed to ball/closedBall`?

@JovanGerb the ball doesn't contain 0 if the radius is 0, so ball doesn't come with any structure, but for closedBall, as @pechersky demonstrated, it is naturally an AddSubgroup (as well as Submodule 𝓞 R).

So maybe the name closedBall can be reserved for the Submodule 𝓞 R?

@adamtopaz What do you think the correct thing to do is? To summarise,

• ball = { x | v x < r } naturally comes with the structure of open set
• closedBall = { x | v x ≤ r } naturally comes with the structure of closed set, AddSubgroup R, and Submodule 𝓞 R.
• sphere = { x | v x = r } naturally comes with the structure of closed set, and SubMulAction 𝒪ˣ R (???).

And I'm asking whether these names (ball, closedBall, sphere) should be bundled with one of the natural structures above.

In private conversations we are now exploring an alternative route via UniformSpace.ball.

I have now made an alternative #27987 for people to decide which one is better.

This pull request has conflicts, please merge master and resolve them.