Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

modified theorem coe_add_monoid_hom'
modified theorem coe_add_monoid_hom
modified theorem coe_monoid_hom'
modified theorem coe_monoid_hom