Def CategoryTheory.TwoSquare.prod

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)
Added CategoryTheory.TwoSquare.prodView on Github →