Commit 2025-02-21 00:07 befd281f

View on Github →

chore(Analysis/Convex/Normed): split into smaller files (#22015) Split Analysis/Convex/Normed into two files, motivated by the desire to get that the (closed) metric ball is convex with fewer imports.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/MeanValue.lean

Modified Mathlib/Analysis/Convex/AmpleSet.lean

Modified Mathlib/Analysis/Convex/Continuous.lean

Modified Mathlib/Analysis/Convex/GaugeRescale.lean

Modified Mathlib/Analysis/Convex/Measure.lean

Modified Mathlib/Analysis/Convex/Side.lean

Modified Mathlib/Analysis/Convex/StrictConvexBetween.lean

Modified Mathlib/Analysis/Convex/StrictConvexSpace.lean

Created Mathlib/Analysis/Normed/Affine/Convex.lean

added theorem Wbtw.dist_add_dist

added theorem dist_add_dist_of_mem_segment

added theorem exists_mem_interior_convexHull_affineBasis

Renamed Mathlib/Analysis/Convex/Normed.lean to Mathlib/Analysis/Normed/Module/Convex.lean

deleted theorem Wbtw.dist_add_dist

deleted theorem dist_add_dist_of_mem_segment

deleted theorem exists_mem_interior_convexHull_affineBasis

Modified Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

Modified Mathlib/Geometry/Manifold/IsManifold/Basic.lean

Modified Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

Modified Mathlib/Geometry/Manifold/Metrizable.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/NumberTheory/EulerProduct/ExpLog.lean