Commit 2025-12-15 19:23 5c208fb4

View on Github →

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

Estimated changes

Modified Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

Modified Mathlib/AlgebraicTopology/SimplicialCategory/SimplicialObject.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/Split.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

modified def SSet.Truncated.hoFunctor₂

Modified Mathlib/AlgebraicTopology/SimplicialSet/HornColimits.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean