Theorem SSet.HomotopyCategory.hom_rec

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.hom_recView on Github →