mathlib

59653709 - feat(data/monoid_algebra): algebra structure, lift of morphisms (#2366)

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. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>