mathlib

aba31c93 - feat(algebra/monoid_algebra): define a non-commutative version of `lift` (#4725)

feat(algebra/monoid_algebra): define a non-commutative version of `lift` (#4725) * [X] define `monoid_algebra.lift_c` and `add_monoid_algebra.lift_nc` to be generalizations of `(mv_)polynomial.eval₂` to `(add_)monoid_algebra`s. * [X] use `to_additive` in many proofs about `add_monoid_algebra`; * [X] define `finsupp.nontrivial`, use it for `(add_)monoid_algebra.nontrivial`; * [X] copy more lemmas about `lift` from `monoid_algebra` to `add_monoid_algebra`; * [X] use `@[ext]` on more powerful type-specific lemmas; * [x] fix docstrings of `(add_)monoid_algebra.lift₂`; * [x] fix compile failures.