Commit 2025-12-16 09:51 72eadd61

View on Github →

chore(Data): fix whitespace (#32931)

Estimated changes

Modified Mathlib/Data/Complex/Basic.lean

modified theorem Complex.im_mul_ofReal

modified theorem Complex.re_mul_ofReal

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/EReal/Basic.lean

Modified Mathlib/Data/Fin/Fin2.lean

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finset/Sort.lean

modified theorem Finset.sort_val

Modified Mathlib/Data/Finsupp/Interval.lean

modified theorem Finsupp.card_Icc

Modified Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

Modified Mathlib/Data/Fintype/List.lean

Modified Mathlib/Data/Fintype/Option.lean

Modified Mathlib/Data/Fintype/Quotient.lean

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/List/Pairwise.lean

Modified Mathlib/Data/List/PeriodicityLemma.lean

Modified Mathlib/Data/List/Pi.lean

Modified Mathlib/Data/Matrix/Mul.lean

Modified Mathlib/Data/Nat/Choose/Factorization.lean

Modified Mathlib/Data/Nat/Digits/Defs.lean

modified theorem Nat.nat_repr_len_aux

Modified Mathlib/Data/Nat/Digits/Lemmas.lean

Modified Mathlib/Data/Nat/MaxPowDiv.lean

Modified Mathlib/Data/Nat/ModEq.lean

modified theorem Nat.ModEq.cancel_left_div_gcd

Modified Mathlib/Data/Nat/Prime/Defs.lean

Modified Mathlib/Data/PFunctor/Multivariate/M.lean

Modified Mathlib/Data/PFunctor/Univariate/M.lean

Modified Mathlib/Data/Real/ConjExponents.lean

Modified Mathlib/Data/Real/Embedding.lean

modified theorem Archimedean.embedReal_apply

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/Data/TypeVec.lean

Modified Mathlib/Data/WSeq/Relation.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/Data/ZMod/Units.lean