Commit 2026-01-07 17:16 a2883f0f

View on Github →

chore: fix even more spacing issues (#33716) Found by extending the commandStart linter to proof bodies in #30658.

Estimated changes

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean

modified theorem CategoryTheory.Abelian.Ext.mapExactFunctor_zero

Modified Mathlib/Algebra/Polynomial/Splits.lean

Modified Mathlib/AlgebraicGeometry/Artinian.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Presentable.lean

Modified Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Distribution/TemperedDistribution.lean

modified theorem TemperedDistribution.smulLeftCLM_const

Modified Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean

Modified Mathlib/Analysis/Matrix/Normed.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

Modified Mathlib/CategoryTheory/LocallyCartesianClosed/ExponentiableMorphism.lean

Modified Mathlib/CategoryTheory/LocallyCartesianClosed/Sections.lean

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

Modified Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/VertexCover.lean

Modified Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

Modified Mathlib/Data/Nat/Digits/Lemmas.lean

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean

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

Modified Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean

Modified Mathlib/MeasureTheory/Integral/MeanValue.lean

Modified Mathlib/NumberTheory/SiegelsLemma.lean

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

Modified Mathlib/RingTheory/Polynomial/IsIntegral.lean

Modified Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

Modified Mathlib/Topology/Separation/Profinite.lean