Theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id

Modification history

2026-01-12 14:46
Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean
feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor` (#31325) …
Added SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_idView on Github →