Theorem CategoryTheory.SimplicialObject.δ_def

Modification history

2025-11-04 11:56
Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
feat(AlgebraicTopology): basic missing lemmas about the simplex category (#31248)
Added CategoryTheory.SimplicialObject.δ_defView on Github →