Theorem CategoryTheory.Functor.Initial.hasLimit_comp_iff

Modification history

2025-10-29 00:04
Mathlib/CategoryTheory/Limits/Final.lean
feat(CategoryTheory): Guitart exact squares and Kan extensions (#30382) …
Added CategoryTheory.Functor.Initial.hasLimit_comp_iffView on Github →