Def CategoryTheory.TwoSquare.StructuredArrowRightwards.prodEquivalence.functor

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.functor View on Github →