Theorem CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt.of_natIso

Modification history

2026-05-28 11:18
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
chore(CategoryTheory/Functor): pointwise Kan extensions under isomorphisms (#39883) …
Added CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt.of_natIsoView on Github →