Commit 2025-05-14 16:52 655d8801

View on Github →

chore: fix more odd indentation (#24906)

Estimated changes

Modified Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

Modified Counterexamples/Pseudoelement.lean

Modified Mathlib/Algebra/AddTorsor/Defs.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

Modified Mathlib/Algebra/Quotient.lean