Theorem CategoryTheory.Functor.hasRightExtension_iff_of_iso₁

Modification history

2024-02-11 09:45
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory): the typeclass Functor.HasRightKanExtension (#10384) …
Added CategoryTheory.Functor.hasRightExtension_iff_of_iso₁View on Github →