Def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functorObj

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.prodEquivalence.functorObjView on Github →