Commit 2025-07-15 09:22 6c0e8529

View on Github →

chore: remove whitespace (#26963) Found by #26926.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Lattice.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Modified Mathlib/Algebra/Order/Group/Defs.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/Matrix/Invertible.lean

Modified Mathlib/Data/Nat/Factorial/Basic.lean

modified theorem Nat.ascFactorial_le_pow_add

modified theorem Nat.two_pow_mul_factorial_le_factorial_two_mul

Modified Mathlib/Data/Ordmap/Ordnode.lean

Modified Mathlib/Data/Set/Image.lean

modified theorem Set.range_inl

modified theorem Set.range_inr

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

modified theorem Basis.coe_ofVectorSpace

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/Logic/Hydra.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

Modified Mathlib/NumberTheory/FLT/Four.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

Modified Mathlib/NumberTheory/NumberField/DedekindZeta.lean

Modified Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

Modified Mathlib/NumberTheory/RamificationInertia/Unramified.lean

Modified Mathlib/NumberTheory/SiegelsLemma.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

Modified Mathlib/Order/Filter/Lift.lean

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

Modified Mathlib/Probability/Kernel/CondDistrib.lean

Modified Mathlib/Probability/Moments/ComplexMGF.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/MvPowerSeries/Trunc.lean

Modified Mathlib/RingTheory/PowerSeries/Trunc.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/RingTheory/Valuation/RankOne.lean