Commit 2026-01-07 14:55 927ddb08

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Basic.lean

Modified Mathlib/Analysis/BoxIntegral/UnitPartition.lean

Modified Mathlib/Analysis/Calculus/ParametricIntegral.lean

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Analysis/Complex/Hadamard.lean

Modified Mathlib/Analysis/Complex/Liouville.lean

Modified Mathlib/Analysis/Complex/PhragmenLindelof.lean

Modified Mathlib/Analysis/Complex/SummableUniformlyOn.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Distribution/TemperateGrowth.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

modified theorem fourier_add

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/Fourier/Inversion.lean

Modified Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

Modified Mathlib/Analysis/InnerProductSpace/Harmonic/Constructions.lean

Modified Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean

Modified Mathlib/Analysis/InnerProductSpace/NormPow.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/Matrix/Order.lean

Modified Mathlib/Analysis/MellinTransform.lean

Modified Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Modified Mathlib/Analysis/Real/Pi/Irrational.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

modified theorem Complex.norm_log_one_add_half_le_self

Modified Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

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

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

Modified Mathlib/Geometry/Manifold/PoincareConjecture.lean

Modified Mathlib/Geometry/Manifold/Riemannian/PathELength.lean

Modified Mathlib/MeasureTheory/Function/AbsolutelyContinuous.lean

Modified Mathlib/MeasureTheory/Function/JacobianOneDim.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Unique.lean

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/MeasureTheory/Measure/Prokhorov.lean

Modified Mathlib/MeasureTheory/Measure/Tight.lean

Modified Mathlib/NumberTheory/AbelSummation.lean

Modified Mathlib/NumberTheory/Chebyshev.lean

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/NumberTheory/ZetaValues.lean

Modified Mathlib/Probability/Moments/CovarianceBilinDual.lean