@[simp]

theorem MonoidAlgebra.linearCombination_of {R : Type u_1} {M : Type u_2} [Semiring R] [MulOneClass M] : Finsupp.linearCombination R ⇑(of R M) = LinearMap.id

@[simp]

theorem AddMonoidAlgebra.linearCombination_of {R : Type u_1} {M : Type u_2} [Semiring R] [AddZeroClass M] : Finsupp.linearCombination R ⇑(of R M) = LinearMap.id

@[simp]

theorem MonoidAlgebra.coe_add {k : Type u₁} {G : Type u₂} [Semiring k] (f g : MonoidAlgebra k G) : ⇑(f + g) = ⇑f + ⇑g

theorem MonoidAlgebra.induction_linear {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G) (zero : p 0) (add : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)) (single : ∀ (a : G) (b : k), p (single a b)) : p f

@[simp]

theorem MonoidAlgebra.liftNCRingHom_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid G] [Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) (a : G) (b : k) : (liftNCRingHom f g h_comm) (single a b) = f b * g a

noncomputable def MonoidAlgebra.mapRangeRingHom {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] [Semiring R] [Semiring S] (f : R →+* S) : MonoidAlgebra R M →+* MonoidAlgebra S M

The ring homomorphism of monoid algebras induced by a homomorphism of the base rings.

Equations

• MonoidAlgebra.mapRangeRingHom f = MonoidAlgebra.liftNCRingHom (MonoidAlgebra.singleOneRingHom.comp f) (MonoidAlgebra.of S M) ⋯

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] [Semiring R] [Semiring S] (f : R →+* S) (x : MonoidAlgebra R M) (m : M) : ((mapRangeRingHom f) x) m = f (x m)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_single {R : Type u_1} {S : Type u_2} {M : Type u_3} [Monoid M] [Semiring R] [Semiring S] (f : R →+* S) (a : M) (b : R) : (mapRangeRingHom f) (single a b) = single a (f b)