Commit 2025-12-15 22:35 fe3134f0

View on Github →

chore(Geometry): fix whitespace (#32904) Extracted from https://github.com/leanprover-community/mathlib4/pull/30658. Found by extending the commandStart linter to proof bodies.

Estimated changes

Modified Mathlib/Geometry/Convex/Cone/Basic.lean

Modified Mathlib/Geometry/Euclidean/Sphere/Basic.lean

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

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/GroupLieAlgebra.lean

Modified Mathlib/Geometry/Manifold/Immersion.lean

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

modified theorem ModelWithCorners.compl_boundary

modified theorem ModelWithCorners.compl_interior

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

Modified Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

Modified Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

modified theorem IsLocalFrameOn.coeff_sum_eq

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

Modified Mathlib/Geometry/Manifold/VectorField/Pullback.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean