Theorem CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimit

Modification history

2025-10-28 23:08
Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) …
Added CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimitView on Github →