2024-10-04 11:14
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
feat(CategoryTheory): lemmas about `descOfIsLeftKanExtension` for pointwise left Kan extensions (+dual) (#17383)
Added CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app