Commit 2026-02-08 20:32 2c514833

View on Github →

chore(RingTheory/TensorProduct): make Algebra.TensorProduct.assoc more linear (#34947) We also remove two unused aux lemmas that can be recovered by the multiplicative properties of Algebra.TensorProduct.assoc.

Estimated changes

Modified Mathlib/Algebra/Category/AlgCat/Monoidal.lean

Modified Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean

modified theorem CommAlgCat.associator_hom_hom

modified theorem CommAlgCat.associator_inv_hom

Modified Mathlib/RingTheory/Bialgebra/Basic.lean

Modified Mathlib/RingTheory/Bialgebra/TensorProduct.lean

Modified Mathlib/RingTheory/TensorProduct/Maps.lean

deleted theorem Algebra.TensorProduct.assoc_aux_1

deleted theorem Algebra.TensorProduct.assoc_aux_2