Theorem CategoryTheory.Functor.HasLeftKanExtension.mk

Modification history

2024-04-20 18:50
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory): the left Kan extension functor (#12168) …
Modified CategoryTheory.Functor.HasLeftKanExtension.mkView on Github →
2024-02-11 09:45
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory): the typeclass Functor.HasRightKanExtension (#10384) …
Added CategoryTheory.Functor.HasLeftKanExtension.mkView on Github →