Commit 2026-01-03 17:21 3eee3750

View on Github →

feat(RingTheory/TensorProduct/MonoidAlgebra): additivise (#33482) This will be used to golf the corresponding MvPolynomial file.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Module.lean

Modified Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean

added theorem AddMonoidAlgebra.tensorEquiv.invFun_tmul

added def MonoidAlgebra.tensorEquiv.invFun

added theorem MonoidAlgebra.tensorEquiv.invFun_tmul