Def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.postcompose

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.RightExtension.IsPointwiseRightKanExtension.postcompose View on Github →