Commit 2025-11-16 20:03 8d0f752e

View on Github →

feat: monoid algebras commute with base change (#29539) From Toric

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem MonoidAlgebra.algebraMap_def

added theorem MonoidAlgebra.symm_mapRangeAlgEquiv

Created Mathlib/RingTheory/TensorProduct/MonoidAlgebra.lean

added theorem MonoidAlgebra.scalarTensorEquiv_symm_single

added theorem MonoidAlgebra.scalarTensorEquiv_tmul

added theorem MonoidAlgebra.tensorEquiv_symm_single

added theorem MonoidAlgebra.tensorEquiv_tmul