mathlib3

91cbe460 - feat(algebra/monoid_algebra/basic): lifts of (add_)monoid_algebras (#13382)

feat(algebra/monoid_algebra/basic): lifts of (add_)monoid_algebras (#13382) We show that homomorphisms of the grading (add) monoids of (add) monoid algebras lift to ring/algebra homs of the algebras themselves. This PR is preparation for introducing Laurent polynomials (see [adomani_laurent_polynomials](https://github.com/leanprover-community/mathlib/tree/adomani_laurent_polynomials), file `data/polynomial/laurent` for a preliminary version). [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Laurent.20polynomials) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>