Theorem CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq

Modification history

2026-03-19 13:59
Mathlib/AlgebraicTopology/SimplicialObject/ChainHomotopy.lean
feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy (#32881) …
Added CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eqView on Github →