Commit 2025-04-01 16:01 f18d5e76

View on Github →

feat(MonoidAlgebra): mapDomain f is injective if f is (#23482) Also rename variable so that k isn't a semiring and G isn't a monoid. From Toric

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

added theorem AddMonoidAlgebra.mapDomain_injective

modified theorem AddMonoidAlgebra.mapDomain_single

modified theorem AddMonoidAlgebra.mapDomain_sum

added theorem MonoidAlgebra.mapDomain_injective

added theorem MonoidAlgebra.mapDomain_single

modified theorem MonoidAlgebra.mapDomain_sum

Modified Mathlib/Algebra/MvPolynomial/Rename.lean