Theorem TopCat.associator_hom_apply_2_2

Modification history

2026-03-25 06:04

Mathlib/Topology/Category/TopCat/Monoidal.lean

feat(Topology/Category): `TopCat` is cartesian monoidal (#37097)

Added TopCat.associator_hom_apply_2_2 View on Github →