Theorem CommAlgCat.associator_hom_hom

Modification history

2026-02-08 20:32
Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean
chore(RingTheory/TensorProduct): make `Algebra.TensorProduct.assoc` more linear (#34947) …
Modified CommAlgCat.associator_hom_homView on Github →
2025-07-11 11:47
Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean
feat: `CommAlgCat` is cocartesian-monoidal (#25365) …
Added CommAlgCat.associator_hom_homView on Github →