Theorem CategoryTheory.Functor.limitIsoOfIsRightKanExtension_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.limitIsoOfIsRightKanExtension_inv_πView on Github →