Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-03 05:00 9e455c15

View on Github →

feat(data/monoid_algebra): Allow R ≠ k in semimodule R (monoid_algebra k G) (#4365) Also does the same for the additive version semimodule R (add_monoid_algebra k G).

Estimated changes

Modified src/algebra/monoid_algebra.lean

modified theorem add_monoid_algebra.alg_hom_ext

modified theorem add_monoid_algebra.alg_hom_ext_iff

modified def add_monoid_algebra.algebra_map'

modified theorem add_monoid_algebra.coe_algebra_map

modified def add_monoid_algebra.lift

modified theorem monoid_algebra.alg_hom_ext

modified theorem monoid_algebra.coe_algebra_map

modified def monoid_algebra.lift

modified theorem monoid_algebra.lift_apply

modified theorem monoid_algebra.lift_of

modified theorem monoid_algebra.lift_single

modified theorem monoid_algebra.lift_symm_apply

modified theorem monoid_algebra.lift_unique'

modified theorem monoid_algebra.lift_unique

added theorem monoid_algebra.single_algebra_map_eq_algebra_map_mul_of