Commit 2025-12-22 13:19 6ef489ef

View on Github →

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

Estimated changes

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/Nat/BitIndices.lean

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

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

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

Modified Mathlib/Data/Nat/MaxPowDiv.lean

modified theorem Nat.maxPowDiv.go_succ

Modified Mathlib/Data/Nat/ModEq.lean

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

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

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

Modified Mathlib/Data/Seq/Basic.lean

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/Data/ZMod/Basic.lean