Commit 2025-09-02 20:18 2f025263

View on Github →

chore(Analysis/{NormedSpace,Normed/Module/Ball}): move files (#29261) This moves / renames the following files in Analysis/NormedSpace/ to Analysis/Normed/Module/Ball/

BallAction → Action
HomeomorphBall → Homeomorph
Pointwise → Pointwise
SphereNormEquiv → RadialEquiv This is part of #28698 to migrate the material in Analysis/NormedSpace/ to other locations.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Tietze.lean

Modified Mathlib/Analysis/Complex/UnitDisc/Basic.lean

Modified Mathlib/Analysis/Convex/Gauge.lean

Modified Mathlib/Analysis/Convex/StrictConvexSpace.lean

Modified Mathlib/Analysis/InnerProductSpace/Calculus.lean

Modified Mathlib/Analysis/Normed/Group/AddCircle.lean

Renamed Mathlib/Analysis/NormedSpace/BallAction.lean to Mathlib/Analysis/Normed/Module/Ball/Action.lean

Renamed Mathlib/Analysis/NormedSpace/HomeomorphBall.lean to Mathlib/Analysis/Normed/Module/Ball/Homeomorph.lean

Renamed Mathlib/Analysis/NormedSpace/Pointwise.lean to Mathlib/Analysis/Normed/Module/Ball/Pointwise.lean

Renamed Mathlib/Analysis/NormedSpace/SphereNormEquiv.lean to Mathlib/Analysis/Normed/Module/Ball/RadialEquiv.lean

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean