# Commit 2020-10-22 07:48 aba31c93

View on Github →feat(algebra/monoid_algebra): define a non-commutative version of `lift`

(#4725)

- define
`monoid_algebra.lift_c`

and`add_monoid_algebra.lift_nc`

to be generalizations of`(mv_)polynomial.eval₂`

to`(add_)monoid_algebra`

s. - use
`to_additive`

in many proofs about`add_monoid_algebra`

; - define
`finsupp.nontrivial`

, use it for`(add_)monoid_algebra.nontrivial`

; - copy more lemmas about
`lift`

from`monoid_algebra`

to`add_monoid_algebra`

; - use
`@[ext]`

on more powerful type-specific lemmas; - fix docstrings of
`(add_)monoid_algebra.lift₂`

; - fix compile failures.