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.