2025-08-26 12:07
Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean
feat(AlgebraicToplogy/SimplexCategory): add notation for faces and degeneracies general truncated simplex categories (#26738)
Added SimplexCategory.Truncated.δ₂_zero_comp_σ₂_one