Commit 2020-04-22 12:16 59653709

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.