Commit 2025-07-11 09:29 f10105b4

View on Github →

chore: a batch of whitespace fixes (#26964) Found by #26926.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

modified def FreeMonoid.freeMonoidCongr

Modified Mathlib/Algebra/Group/Conj.lean

modified theorem IsConj.pow

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

modified theorem Subgroup.coe_subtype

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

modified theorem LinearEquiv.symm_comp

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

modified def Submodule.botEquivPUnit

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

Modified Mathlib/Algebra/Order/Nonneg/Basic.lean

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

Modified Mathlib/Algebra/Regular/SMul.lean

Modified Mathlib/Algebra/Ring/Center.lean

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

Modified Mathlib/Data/Matrix/Mul.lean

modified theorem Matrix.mulVec_neg

modified theorem Matrix.neg_mulVec

modified theorem Matrix.neg_vecMul

modified theorem Matrix.vecMul_neg

Modified Mathlib/Data/Set/Piecewise.lean

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/LinearAlgebra/Prod.lean

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Encodable/Basic.lean

modified theorem Encodable.decode_option_zero

Modified Mathlib/MeasureTheory/Integral/Gamma.lean

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

Modified Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean

Modified Mathlib/ModelTheory/Order.lean

Modified Mathlib/ModelTheory/PartialEquiv.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/Cyclotomic/Three.lean

modified theorem IsCyclotomicExtension.Rat.Three.eta_sq

Modified Mathlib/NumberTheory/EulerProduct/Basic.lean

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/NumberTheory/Harmonic/Bounds.lean

Modified Mathlib/NumberTheory/Harmonic/GammaDeriv.lean

Modified Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

Modified Mathlib/NumberTheory/JacobiSum/Basic.lean

Modified Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

Modified Mathlib/NumberTheory/LSeries/Basic.lean

Modified Mathlib/NumberTheory/LSeries/Convergence.lean

Modified Mathlib/NumberTheory/LSeries/Deriv.lean

Modified Mathlib/NumberTheory/LSeries/Dirichlet.lean

Modified Mathlib/NumberTheory/LSeries/DirichletContinuation.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean

Modified Mathlib/NumberTheory/LSeries/Linearity.lean

modified theorem LSeries.term_sum

Modified Mathlib/NumberTheory/LSeries/Nonvanishing.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/NumberTheory/LSeries/SumCoeff.lean

Modified Mathlib/NumberTheory/LSeries/ZMod.lean

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

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

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean

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

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

Modified Mathlib/NumberTheory/NumberField/EquivReindex.lean

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

modified theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mk_apply

Modified Mathlib/NumberTheory/NumberField/House.lean

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

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

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Modified Mathlib/NumberTheory/NumberField/Units/Regulator.lean

Modified Mathlib/NumberTheory/Ostrowski.lean

modified theorem Rat.AbsoluteValue.eq_on_nat_iff_eq

modified theorem Rat.AbsoluteValue.equiv_on_nat_iff_equiv

Modified Mathlib/NumberTheory/Padics/Complex.lean

modified theorem PadicComplex.coe_natCast

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/NumberTheory/SelbergSieve.lean

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Order/CompleteLattice/Chain.lean

Modified Mathlib/Order/CompletePartialOrder.lean

Modified Mathlib/Order/Cover.lean

modified theorem CovBy.exists_set_sdiff_singleton

Modified Mathlib/Order/Interval/Finset/Defs.lean

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

Modified Mathlib/Order/ScottContinuity.lean

Modified Mathlib/Order/SuccPred/Basic.lean

modified theorem Order.Ico_subset_Ioo_pred_left_of_not_isMin

Modified Mathlib/Probability/Independence/Basic.lean

Modified Mathlib/Probability/Independence/Kernel.lean

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

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Probability/Martingale/OptionalStopping.lean

Modified Mathlib/Probability/Moments/Variance.lean

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

Modified Mathlib/RingTheory/Ideal/Quotient/PowTransition.lean

Modified Mathlib/RingTheory/MvPowerSeries/LexOrder.lean

Modified Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

modified theorem Polynomial.coe_neg

Modified Mathlib/Topology/Algebra/Order/Support.lean

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

Modified Mathlib/Topology/Algebra/Valued/NormedValued.lean

Modified Mathlib/Topology/ContinuousMap/CompactlySupported.lean

modified theorem CompactlySupportedContinuousMap.nnrealPart_neg_toReal_eq