Def CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift

Modification history

2026-01-26 16:58

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

chore(CategoryTheory/Limits): add `IsColimit.nonempty_isColimit_iff_isIso_desc` and golf (#34237) …

Added CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift View on Github →