Theorem CategoryTheory.Functor.LeftExtension.nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff

Modification history

2025-10-29 00:04
Mathlib/CategoryTheory/GuitartExact/KanExtension.lean
feat(CategoryTheory): Guitart exact squares and Kan extensions (#30382) …
Added CategoryTheory.Functor.LeftExtension.nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iffView on Github →