Commit 2025-10-21 20:48 67765741

View on Github →

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

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/LocalRing.lean

Modified Mathlib/RingTheory/Binomial.lean

modified theorem Ring.multichoose_neg_self

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

modified def IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod

modified def IsDedekindDomain.selmerGroup.fromUnitLift

modified def IsDedekindDomain.selmerGroup

Modified Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean

Modified Mathlib/RingTheory/Flat/Domain.lean

Modified Mathlib/RingTheory/Grassmannian.lean

Modified Mathlib/RingTheory/HahnSeries/HEval.lean

Modified Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

Modified Mathlib/RingTheory/Invariant/Basic.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/Localization/Defs.lean

Modified Mathlib/RingTheory/MvPowerSeries/Evaluation.lean

Modified Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean

Modified Mathlib/RingTheory/Nilpotent/Exp.lean

Modified Mathlib/RingTheory/Norm/Transitivity.lean

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

Modified Mathlib/RingTheory/SimpleModule/Isotypic.lean