Theorem SimplexCategory.Truncated.δ₂_one_eq_const

Modification history

2025-12-18 13:14
Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean
refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446) …
Modified SimplexCategory.Truncated.δ₂_one_eq_constView on Github →
2025-11-04 11:56
Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean
feat(AlgebraicTopology): basic missing lemmas about the simplex category (#31248)
Added SimplexCategory.Truncated.δ₂_one_eq_constView on Github →