Theorem SSet.HomotopyCategory.homMk_id

Modification history

2026-08-19 11:50
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
feat(AlgebraicTopology/SimplicialSet): induction principle for morphisms of the homotopy category of a simplicial set (#42673)
Added SSet.HomotopyCategory.homMk_idView on Github →