Theorem CategoryTheory.TwoSquare.hasLeftKanExtension

Modification history

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