Def CategoryTheory.SimplicialObject.Homotopy.whiskerRight

Modification history

2026-03-19 13:59

Mathlib/AlgebraicTopology/SimplicialObject/Homotopy.lean

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

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