2024-10-19 19:08
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
feat(CategoryTheory/KanExtensions): Evaluating `lan` twice amounts to taking a colimit (#17531)
Added CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv