Theorem CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplex

Modification history

2025-10-28 23:08
Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) …
Added CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplexView on Github →