Mathlib Changelog
v4
Changelog
About
Github
Theorem
SimplexCategory.Truncated.δ₂_one_comp_σ₂_one
Modification history
2025-11-04 11:56
Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean
feat(AlgebraicTopology): basic missing lemmas about the simplex category (#31248)
Added
SimplexCategory.Truncated.δ₂_one_comp_σ₂_one
View on Github →