Theorem CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app

Modification history

2025-06-22 16:54
Mathlib/CategoryTheory/Functor/KanExtension/Preserves.lean
feat(CategoryTheory/Functor/KanExtension): preservations of Kan extensions (#25753) …
Added CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_appView on Github →