Theorem CategoryTheory.Functor.hom_ext_of_isLeftKanExtension

Modification history

2024-04-20 18:50
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory): the left Kan extension functor (#12168) …
Modified CategoryTheory.Functor.hom_ext_of_isLeftKanExtensionView on Github →
2024-02-08 08:31
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory/Functor): definition of Kan extensions (#10195) …
Added CategoryTheory.Functor.hom_ext_of_isLeftKanExtensionView on Github →