Commit 2026-04-07 17:30 3ff9e182

View on Github →

chore(AlgebraicTopology): making SimplexCategory a one-field structure (#37734)

Estimated changes

Modified Mathlib/AlgebraicTopology/CechNerve.lean

Modified Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean

deleted theorem SimplexCategory.ext

deleted def SimplexCategory.len

modified theorem SimplexCategory.len_mk

deleted def SimplexCategory.mk

added structure SimplexCategory

deleted def SimplexCategory

Modified Mathlib/AlgebraicTopology/SimplexCategory/Rev.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplexOne.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean