@[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

theorem AddMonoidAlgebra.induction_linear {k : Type u_3} {G : Type u_4} [Semiring k] [AddMonoid G] {p : AddMonoidAlgebra k G → Prop} (f : AddMonoidAlgebra k G) (zero : p 0) (add : ∀ (f g : AddMonoidAlgebra k G), p f → p g → p (f + g)) (single : ∀ (a : G) (b : k), p (single a b)) : p f

noncomputable def MonoidAlgebra.mapRangeRingHom {R : Type u_3} {S : Type u_4} {M : Type u_5} [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_3} {S : Type u_4} {M : Type u_5} [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_3} {S : Type u_4} {M : Type u_5} [Monoid M] [Semiring R] [Semiring S] (f : R →+* S) (a : M) (b : R) : (mapRangeRingHom f) (single a b) = single a (f b)