Def CategoryTheory.TwoSquare

Modification history

2026-10-10 13:11
Mathlib/CategoryTheory/Functor/TwoSquare.lean
feat(CategoryTheory): the external product of two Guitart exact squares is Guitart exact (#43895)
Deleted CategoryTheory.TwoSquareView on Github →
2025-02-27 22:45
Mathlib/CategoryTheory/Functor/TwoSquare.lean
feat(CategoryTheory): 2-squares of functors (#22248) …
Modified CategoryTheory.TwoSquareView on Github →
2024-02-14 00:27
Mathlib/CategoryTheory/GuitartExact.lean
feat(CategoryTheory): Guitart exact squares (#10270) …
Added CategoryTheory.TwoSquareView on Github →