Def SSet.unitHomEquiv

Modification history

2025-02-08 20:13
Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean
feat(AlgebraicTopology): notations X _⦋n⦌ and X ^⦋n⦌ for (co)simplicial objects (#21581) …
Modified SSet.unitHomEquivView on Github →
2024-03-29 21:36
Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean
feat(AlgebraicTopology): the monoidal category structure on simplicial sets (#11396) …
Added SSet.unitHomEquivView on Github →