Commit 2025-12-22 13:19 858a0d95

View on Github →

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

Estimated changes

Modified Mathlib/AlgebraicTopology/DoldKan/Projections.lean

modified theorem AlgebraicTopology.DoldKan.P_succ

Modified Mathlib/AlgebraicTopology/Quasicategory/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/FiniteProd.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

modified def SSet.horn.const