Theorem CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc

Modification history

2026-01-26 16:58
Mathlib/CategoryTheory/Limits/IsLimit.lean
chore(CategoryTheory/Limits): add `IsColimit.nonempty_isColimit_iff_isIso_desc` and golf (#34237) …
Added CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_descView on Github →