Commit 2025-02-17 23:08 c9ab0fe7

View on Github →

chore(whitespace): fix some whitespace (#22006) Following from this Zulip discussion.

Estimated changes

Modified Mathlib/Data/Finsupp/MonomialOrder.lean

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Topology/Algebra/Algebra/Equiv.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

modified def Profinite.NobelingProof.GoodProducts.sum_equiv

modified theorem Profinite.NobelingProof.Products.lt_iff_lex_lt

modified def Profinite.NobelingProof.Products

modified theorem Profinite.NobelingProof.continuous_swapTrue

modified def Profinite.NobelingProof.ord

modified theorem Profinite.NobelingProof.ord_term

modified theorem Profinite.NobelingProof.ord_term_aux

modified def Profinite.NobelingProof.term

modified theorem Profinite.NobelingProof.term_ord_aux

Modified Mathlib/Util/AssertExists.lean