Def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence

Modification history

2026-10-10 13:11
Mathlib/CategoryTheory/GuitartExact/Prod.lean
feat(CategoryTheory): the external product of two Guitart exact squares is Guitart exact (#43895)
Added CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalenceView on Github →