Theorem SSet.HomotopyCategory.rec_mk

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