# Commit 2020-04-22 12:16 59653709

View on Github →feat(data/monoid_algebra): algebra structure, lift of morphisms (#2366)
Prove that for a monoid homomorphism `f : G →* R`

from a monoid `G`

to a `k`

-algebra `R`

there exists a unique algebra morphism `g : k[G] →ₐ[k] R`

such that `∀ x : G, g (single x 1) = f x`

.
This is expressed as `def lift : (G →* R) ≃ (monoid_algebra k G →ₐ[k] R)`

.
I want to use this to define `aeval`

and `eval₂`

for polynomials. This way we'll have many properties for free.