Theorem CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv

Modification history

2024-10-25 21:52
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory/KanExtension): Composing `lan` with `colim` (#17355)
Added CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_invView on Github →