Commit 2025-12-16 21:41 7034fdc0

View on Github →

chore(RingTheory): fix whitespace (#32962) Found by extending the commandStart linter to proof bodies.

Estimated changes

Modified Mathlib/RingTheory/Congruence/Hom.lean

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Modified Mathlib/RingTheory/Etale/StandardEtale.lean

Modified Mathlib/RingTheory/Extension/Presentation/Basic.lean

modified def Algebra.Presentation.baseChange

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

Modified Mathlib/RingTheory/FractionalIdeal/Extended.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

Modified Mathlib/RingTheory/Ideal/Maximal.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/Ideal/Over.lean

modified theorem Ideal.under_under

Modified Mathlib/RingTheory/Ideal/Pointwise.lean

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Localization/Algebra.lean

Modified Mathlib/RingTheory/Localization/BaseChange.lean

Modified Mathlib/RingTheory/Localization/Integer.lean

Modified Mathlib/RingTheory/Localization/Module.lean

Modified Mathlib/RingTheory/MatrixPolynomialAlgebra.lean

Modified Mathlib/RingTheory/MvPolynomial.lean

Modified Mathlib/RingTheory/MvPolynomial/Groebner.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

Modified Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

Modified Mathlib/RingTheory/NormalClosure.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

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

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

Modified Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean

Modified Mathlib/RingTheory/PolynomialLaw/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

Modified Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean

Modified Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangeFree.lean

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

modified theorem AddValuation.map_inv

Modified Mathlib/RingTheory/Valuation/Discrete/Basic.lean

Modified Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean