Theorem CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff

Modification history

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