Theorem CategoryTheory.Functor.HasPointwiseLeftKanExtension.of_iso

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.HasPointwiseLeftKanExtension.of_isoView on Github →