Commit 2025-05-26 13:39 5487f2e2

View on Github →

chore(RingTheory/HopfAlgebra): redo tensor product (#25196) ...without category theory, so that we can easily generalize to the base change of hopf algebras later. This also makes things universe-polymorphic.

Estimated changes

Modified Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

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

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq

Modified Mathlib/RingTheory/Bialgebra/TensorProduct.lean

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

deleted theorem TensorProduct.comul_def

deleted theorem TensorProduct.comul_tmul

deleted theorem TensorProduct.counit_def

deleted theorem TensorProduct.counit_tmul

Modified Mathlib/RingTheory/Coalgebra/TensorProduct.lean

modified theorem Coalgebra.TensorProduct.lid_symm_apply

modified theorem Coalgebra.TensorProduct.lid_tmul

added theorem TensorProduct.comul_def

added theorem TensorProduct.comul_tmul

added theorem TensorProduct.counit_def

added theorem TensorProduct.counit_tmul

Modified Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean