Def CategoryTheory.SimplicialObject.Homotopy.postcomp

Modification history

2026-03-19 13:59

Mathlib/AlgebraicTopology/SimplicialObject/Homotopy.lean

feat(AlgebraicTopology/SimplicialObject): define simplicial homotopy (#32881) …

Added CategoryTheory.SimplicialObject.Homotopy.postcomp View on Github →