Commit 2025-12-27 23:32 cc0ebd15

View on Github →

chore: fix more whitespace formatting (#33342) Found by extending the commandStart linter to proof bodies. Extracted from #30658.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

Modified Mathlib/Algebra/Lie/Sl2.lean

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

Modified Mathlib/Algebra/Polynomial/CoeffMem.lean

Modified Mathlib/Algebra/Polynomial/Roots.lean

Modified Mathlib/Algebra/QuadraticDiscriminant.lean

modified theorem quadratic_ne_zero_of_discrim_ne_sq

Modified Mathlib/Algebra/Vertex/VertexOperator.lean

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Calculus/LogDeriv.lean

Modified Mathlib/Analysis/Calculus/TangentCone/ProperSpace.lean

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

Modified Mathlib/Analysis/LConvolution.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Analysis/Normed/Field/ProperSpace.lean

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

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

Modified Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

Modified Mathlib/Analysis/SpecialFunctions/Choose.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean

Modified Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Types/Pushouts.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Hopf_.lean

Modified Mathlib/CategoryTheory/Monoidal/Mod_.lean

modified theorem CategoryTheory.ModObj.smul_eq_mul

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Skeleton.lean

Modified Mathlib/CategoryTheory/Sites/Descent/DescentData.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

Modified Mathlib/Computability/AkraBazzi/SumTransform.lean

Modified Mathlib/FieldTheory/CardinalEmb.lean

Modified Mathlib/FieldTheory/Perfect.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Basic.lean

Modified Mathlib/Geometry/Euclidean/SignedDist.lean

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

Modified Mathlib/GroupTheory/Archimedean.lean

Modified Mathlib/GroupTheory/QuotientGroup/Defs.lean

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Measure/GiryMonad.lean

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

Modified Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean

Modified Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean

Modified Mathlib/RingTheory/Perfection.lean

Modified Mathlib/RingTheory/Perfectoid/Untilt.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/Tactic/Bound.lean

Modified Mathlib/Topology/Algebra/Module/Cardinality.lean

Modified Mathlib/Topology/Category/Profinite/EffectiveEpi.lean

Modified Mathlib/Topology/Category/Stonean/EffectiveEpi.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Constructible.lean

Modified Mathlib/Topology/Covering/Basic.lean

Modified Mathlib/Topology/Instances/CantorSet.lean

Modified Mathlib/Topology/Semicontinuity/Basic.lean

Modified Mathlib/Topology/VectorBundle/Riemannian.lean