Commit 2025-10-23 00:20 5fdb78b8

View on Github →

style(misc): fix whitespace (#30691) Extracted from #30658. Found by extending the commandStart linter to proof bodies.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

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

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Control/ULiftable.lean

Modified Mathlib/Geometry/Manifold/PoincareConjecture.lean

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

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/Coxeter/Inversion.lean

Modified Mathlib/GroupTheory/Coxeter/Length.lean

Modified Mathlib/GroupTheory/FixedPointFree.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

Modified Mathlib/GroupTheory/GroupAction/Primitive.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Modified Mathlib/GroupTheory/PushoutI.lean

Modified Mathlib/GroupTheory/SpecificGroups/Dihedral.lean

modified theorem DihedralGroup.r_pow

modified theorem DihedralGroup.r_zpow

Modified Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

Modified Mathlib/LinearAlgebra/FreeProduct/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

Modified Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

Modified Mathlib/LinearAlgebra/Matrix/Notation.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean

modified theorem RootPairing.EmbeddedG2.pairing_long_short

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/RootPairingCat.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

Modified Mathlib/LinearAlgebra/Vandermonde.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Logic/Equiv/Option.lean

modified def Equiv.optionEquivSumPUnit.{v,

Modified Mathlib/Logic/Equiv/Prod.lean

modified def Equiv.uniqueSigma

Modified Mathlib/Logic/Function/Iterate.lean

Modified Mathlib/Logic/Small/Defs.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Function/Holder.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

Modified Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

Modified Mathlib/ModelTheory/Syntax.lean

Modified Mathlib/NumberTheory/Dioph.lean

Modified Mathlib/NumberTheory/FLT/Basic.lean

Modified Mathlib/NumberTheory/FLT/MasonStothers.lean

Modified Mathlib/NumberTheory/FLT/Three.lean

Modified Mathlib/NumberTheory/FactorisationProperties.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/NumberTheory/PellMatiyasevic.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/Probability/Distributions/Gamma.lean

Modified Mathlib/Probability/Distributions/Gaussian/Real.lean

Modified Mathlib/Probability/Distributions/Geometric.lean

modified def ProbabilityTheory.geometricPMFReal

Modified Mathlib/Probability/Distributions/Poisson.lean

modified def ProbabilityTheory.poissonPMFReal

Modified Mathlib/Probability/Independence/Conditional.lean

Modified Mathlib/Probability/Independence/ZeroOne.lean

Modified Mathlib/Probability/Kernel/Condexp.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/Kernel/WithDensity.lean

Modified Mathlib/Probability/Moments/Basic.lean

modified theorem ProbabilityTheory.mgf_add_const

Modified Mathlib/Probability/Moments/Covariance.lean

modified theorem ProbabilityTheory.covariance_fun_neg_left

modified theorem ProbabilityTheory.covariance_fun_neg_right

Modified Mathlib/Probability/Moments/IntegrableExpMul.lean

Modified Mathlib/Probability/Moments/MGFAnalytic.lean

Modified Mathlib/Probability/Moments/SubGaussian.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

Modified Mathlib/Probability/StrongLaw.lean

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

Modified Mathlib/RepresentationTheory/Homological/Resolution.lean

Modified Mathlib/SetTheory/Cardinal/Defs.lean

modified theorem Cardinal.mk_arrow

Modified Mathlib/Tactic/ApplyAt.lean

Modified Mathlib/Tactic/FastInstance.lean

Modified Mathlib/Topology/Algebra/Constructions/DomMulAct.lean

Modified Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

Modified Mathlib/Topology/UniformSpace/Defs.lean

Modified Mathlib/Topology/VectorBundle/Riemannian.lean