Monoid algebras

When the domain of a Finsupp has a multiplicative or additive structure, we can define a convolution product. To mathematicians this structure is known as the "monoid algebra", i.e. the finite formal linear combinations over a given semiring of elements of a monoid M. The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.

In fact the construction of the "monoid algebra" makes sense when M is not even a monoid, but merely a magma, i.e., when M carries a multiplication which is not required to satisfy any conditions at all. In this case the construction yields a not-necessarily-unital, not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such algebras to magmas, and we prove this as MonoidAlgebra.liftMagma.

In this file we define MonoidAlgebra R M := M →₀ R, and AddMonoidAlgebra R M in the same way, and then define the convolution product on these.

When the domain is additive, this is used to define polynomials:

Polynomial R := AddMonoidAlgebra R ℕ
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)

Note: Polynomial R is currently a wrapper around AddMonoidAlgebra R ℕ and not defeq to it. There is ongoing work to make it defeq. See https://github.com/leanprover-community/mathlib4/pull/25273

When the domain is multiplicative, e.g. a group, this will be used to define the group ring.

Notation

We introduce the notation R[M] for both MonoidAlgebra R M and AddMonoidAlgebra R M. The notations are scoped to their respective namespaces, and which one R[M] resolves to therefore depends on which of the two namespaces is open.

TODO

Use coeff/ofCoeff more widely. See https://github.com/leanprover-community/mathlib4/pull/36746 https://github.com/leanprover-community/mathlib4/pull/25273

def MonoidAlgebra (R : Type u_8) (M : Type u_9) [Semiring R] : Type (max u_8 u_9)

The monoid algebra over a semiring R generated by the monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

def AddMonoidAlgebra (R : Type u_8) (M : Type u_9) [Semiring R] : Type (max u_8 u_9)

The additive monoid algebra over a semiring R generated by the additive monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

def AddMonoidAlgebra.«term__[_]» : Lean.TrailingParserDescr

The additive monoid algebra over a semiring R generated by the additive monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

def AddMonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for AddMonoidAlgebra.

def MonoidAlgebra.«term__[_]» : Lean.TrailingParserDescr

The monoid algebra over a semiring R generated by the monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

def MonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for MonoidAlgebra.

def MonoidAlgebra.ofCoeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : MonoidAlgebra R M

Construct an element of the monoid algebra R[M] from its coefficients M →₀ R.

def AddMonoidAlgebra.ofCoeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : AddMonoidAlgebra R M

Construct an element of the additive monoid algebra R[M] from its coefficients M →₀ R.

def MonoidAlgebra.coeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : MonoidAlgebra R M) : M →₀ R

The coefficients M →₀ R of an element of the monoid algebra R[M].

def AddMonoidAlgebra.coeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : AddMonoidAlgebra R M) : M →₀ R

The coefficients M →₀ R of an element of the additive monoid algebra R[M].

@[simp]

theorem MonoidAlgebra.coeff_ofCoeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : (ofCoeff x).coeff = x

@[simp]

theorem AddMonoidAlgebra.coeff_ofCoeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : (ofCoeff x).coeff = x

@[simp]

theorem MonoidAlgebra.ofCoeff_coeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : MonoidAlgebra R M) : ofCoeff x.coeff = x

@[simp]

theorem AddMonoidAlgebra.ofCoeff_coeff {R : Type u_1} {M : Type u_4} [Semiring R] (x : AddMonoidAlgebra R M) : ofCoeff x.coeff = x

def MonoidAlgebra.coeffEquiv {R : Type u_1} {M : Type u_4} [Semiring R] : MonoidAlgebra R M ≃ (M →₀ R)

MonoidAlgebra.coeff as an equiv.

def AddMonoidAlgebra.coeffEquiv {R : Type u_1} {M : Type u_4} [Semiring R] : AddMonoidAlgebra R M ≃ (M →₀ R)

AddMonoidAlgebra.coeff as an equiv.

@[simp]

theorem MonoidAlgebra.coeffEquiv_symm_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : coeffEquiv.symm x = ofCoeff x

@[simp]

theorem AddMonoidAlgebra.coeffEquiv_symm_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : coeffEquiv.symm x = ofCoeff x

@[simp]

theorem AddMonoidAlgebra.coeffEquiv_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : AddMonoidAlgebra R M) : coeffEquiv x = x.coeff

@[simp]

theorem MonoidAlgebra.coeffEquiv_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : MonoidAlgebra R M) : coeffEquiv x = x.coeff

theorem MonoidAlgebra.forall {R : Type u_1} {M : Type u_4} [Semiring R] {P : MonoidAlgebra R M → Prop} : (∀ (p : MonoidAlgebra R M), P p) ↔ ∀ (q : M →₀ R), P (ofCoeff q)

theorem AddMonoidAlgebra.forall {R : Type u_1} {M : Type u_4} [Semiring R] {P : AddMonoidAlgebra R M → Prop} : (∀ (p : AddMonoidAlgebra R M), P p) ↔ ∀ (q : M →₀ R), P (ofCoeff q)

theorem MonoidAlgebra.exists {R : Type u_1} {M : Type u_4} [Semiring R] {P : MonoidAlgebra R M → Prop} : (∃ (p : MonoidAlgebra R M), P p) ↔ ∃ (q : M →₀ R), P (ofCoeff q)

theorem AddMonoidAlgebra.exists {R : Type u_1} {M : Type u_4} [Semiring R] {P : AddMonoidAlgebra R M → Prop} : (∃ (p : AddMonoidAlgebra R M), P p) ↔ ∃ (q : M →₀ R), P (ofCoeff q)

theorem MonoidAlgebra.coeff_injective {R : Type u_1} {M : Type u_4} [Semiring R] : Function.Injective coeff

theorem AddMonoidAlgebra.coeff_injective {R : Type u_1} {M : Type u_4} [Semiring R] : Function.Injective coeff

theorem MonoidAlgebra.ofCoeff_injective {R : Type u_1} {M : Type u_4} [Semiring R] : Function.Injective ofCoeff

theorem AddMonoidAlgebra.ofCoeff_injective {R : Type u_1} {M : Type u_4} [Semiring R] : Function.Injective ofCoeff

@[simp]

theorem MonoidAlgebra.coeff_inj {R : Type u_1} {M : Type u_4} [Semiring R] {x y : MonoidAlgebra R M} : x.coeff = y.coeff ↔ x = y

@[simp]

theorem AddMonoidAlgebra.coeff_inj {R : Type u_1} {M : Type u_4} [Semiring R] {x y : AddMonoidAlgebra R M} : x.coeff = y.coeff ↔ x = y

theorem MonoidAlgebra.ofCoeff_inj {R : Type u_1} {M : Type u_4} [Semiring R] {x y : M →₀ R} : ofCoeff x = ofCoeff y ↔ x = y

theorem AddMonoidAlgebra.ofCoeff_inj {R : Type u_1} {M : Type u_4} [Semiring R] {x y : M →₀ R} : ofCoeff x = ofCoeff y ↔ x = y

@[implicit_reducible]

instance MonoidAlgebra.inhabited {R : Type u_1} {M : Type u_4} [Semiring R] : Inhabited (MonoidAlgebra R M)

@[implicit_reducible]

instance AddMonoidAlgebra.inhabited {R : Type u_1} {M : Type u_4} [Semiring R] : Inhabited (AddMonoidAlgebra R M)

instance MonoidAlgebra.nontrivial {R : Type u_1} {M : Type u_4} [Semiring R] [Nontrivial R] [Nonempty M] : Nontrivial (MonoidAlgebra R M)

instance AddMonoidAlgebra.nontrivial {R : Type u_1} {M : Type u_4} [Semiring R] [Nontrivial R] [Nonempty M] : Nontrivial (AddMonoidAlgebra R M)

@[implicit_reducible]

instance MonoidAlgebra.unique {R : Type u_1} {M : Type u_4} [Semiring R] [Subsingleton R] : Unique (MonoidAlgebra R M)

@[implicit_reducible]

instance AddMonoidAlgebra.unique {R : Type u_1} {M : Type u_4} [Semiring R] [Subsingleton R] : Unique (AddMonoidAlgebra R M)

@[implicit_reducible]

instance MonoidAlgebra.instDecidableEq {R : Type u_1} {M : Type u_4} [Semiring R] [DecidableEq R] [DecidableEq M] : DecidableEq (MonoidAlgebra R M)

@[implicit_reducible]

instance AddMonoidAlgebra.instDecidableEq {R : Type u_1} {M : Type u_4} [Semiring R] [DecidableEq R] [DecidableEq M] : DecidableEq (AddMonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.addCommMonoid {R : Type u_1} {M : Type u_4} [Semiring R] : AddCommMonoid (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.addAddCommMonoid {R : Type u_1} {M : Type u_4} [Semiring R] : AddCommMonoid (AddMonoidAlgebra R M)

instance MonoidAlgebra.instIsCancelAdd {R : Type u_1} {M : Type u_4} [Semiring R] [IsCancelAdd R] : IsCancelAdd (MonoidAlgebra R M)

instance AddMonoidAlgebra.instIsCancelAdd {R : Type u_1} {M : Type u_4} [Semiring R] [IsCancelAdd R] : IsCancelAdd (AddMonoidAlgebra R M)

@[implicit_reducible]

instance MonoidAlgebra.instCoeFun {R : Type u_1} {M : Type u_4} [Semiring R] : CoeFun (MonoidAlgebra R M) fun (x : MonoidAlgebra R M) => M → R

@[implicit_reducible]

instance AddMonoidAlgebra.instCoeFun {R : Type u_1} {M : Type u_4} [Semiring R] : CoeFun (AddMonoidAlgebra R M) fun (x : AddMonoidAlgebra R M) => M → R

theorem MonoidAlgebra.ext {R : Type u_1} {M : Type u_4} [Semiring R] ⦃f g : MonoidAlgebra R M⦄ (hfg : ∀ (m : M), f m = g m) : f = g

A copy of Finsupp.ext for MonoidAlgebra.

theorem AddMonoidAlgebra.ext {R : Type u_1} {M : Type u_4} [Semiring R] ⦃f g : AddMonoidAlgebra R M⦄ (hfg : ∀ (m : M), f m = g m) : f = g

A copy of Finsupp.ext for AddMonoidAlgebra.

theorem AddMonoidAlgebra.ext_iff {R : Type u_1} {M : Type u_4} [Semiring R] {f g : AddMonoidAlgebra R M} : f = g ↔ ∀ (m : M), f m = g m

theorem MonoidAlgebra.ext_iff {R : Type u_1} {M : Type u_4} [Semiring R] {f g : MonoidAlgebra R M} : f = g ↔ ∀ (m : M), f m = g m

noncomputable def MonoidAlgebra.coeffAddEquiv {R : Type u_1} {M : Type u_4} [Semiring R] : MonoidAlgebra R M ≃+ (M →₀ R)

MonoidAlgebra.coeff as an AddEquiv.

noncomputable def AddMonoidAlgebra.coeffAddEquiv {R : Type u_1} {M : Type u_4} [Semiring R] : AddMonoidAlgebra R M ≃+ (M →₀ R)

AddMonoidAlgebra.coeff as an AddEquiv.

@[simp]

theorem AddMonoidAlgebra.coeffAddEquiv_symm_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : coeffAddEquiv.symm x = ofCoeff x

@[simp]

theorem MonoidAlgebra.coeffAddEquiv_symm_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : M →₀ R) : coeffAddEquiv.symm x = ofCoeff x

@[simp]

theorem AddMonoidAlgebra.coeffAddEquiv_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : AddMonoidAlgebra R M) : coeffAddEquiv x = x.coeff

@[simp]

theorem MonoidAlgebra.coeffAddEquiv_apply {R : Type u_1} {M : Type u_4} [Semiring R] (x : MonoidAlgebra R M) : coeffAddEquiv x = x.coeff

@[simp]

theorem MonoidAlgebra.coeff_zero {R : Type u_1} {M : Type u_4} [Semiring R] : coeff 0 = 0

@[simp]

theorem AddMonoidAlgebra.coeff_zero {R : Type u_1} {M : Type u_4} [Semiring R] : coeff 0 = 0

@[simp]

theorem MonoidAlgebra.ofCoeff_zero {R : Type u_1} {M : Type u_4} [Semiring R] : ofCoeff 0 = 0

@[simp]

theorem AddMonoidAlgebra.ofCoeff_zero {R : Type u_1} {M : Type u_4} [Semiring R] : ofCoeff 0 = 0

@[simp]

theorem MonoidAlgebra.coeff_eq_zero {R : Type u_1} {M : Type u_4} [Semiring R] {x : MonoidAlgebra R M} : x.coeff = 0 ↔ x = 0

@[simp]

theorem AddMonoidAlgebra.coeff_eq_zero {R : Type u_1} {M : Type u_4} [Semiring R] {x : AddMonoidAlgebra R M} : x.coeff = 0 ↔ x = 0

@[simp]

theorem MonoidAlgebra.ofCoeff_eq_zero {R : Type u_1} {M : Type u_4} [Semiring R] {x : M →₀ R} : ofCoeff x = 0 ↔ x = 0

@[simp]

theorem AddMonoidAlgebra.ofCoeff_eq_zero {R : Type u_1} {M : Type u_4} [Semiring R] {x : M →₀ R} : ofCoeff x = 0 ↔ x = 0

@[simp]

theorem MonoidAlgebra.coeff_add {R : Type u_1} {M : Type u_4} [Semiring R] (x y : MonoidAlgebra R M) : (x + y).coeff = x.coeff + y.coeff

@[simp]

theorem AddMonoidAlgebra.coeff_add {R : Type u_1} {M : Type u_4} [Semiring R] (x y : AddMonoidAlgebra R M) : (x + y).coeff = x.coeff + y.coeff

@[simp]

theorem MonoidAlgebra.ofCoeff_add {R : Type u_1} {M : Type u_4} [Semiring R] (x y : M →₀ R) : ofCoeff (x + y) = ofCoeff x + ofCoeff y

@[simp]

theorem AddMonoidAlgebra.ofCoeff_add {R : Type u_1} {M : Type u_4} [Semiring R] (x y : M →₀ R) : ofCoeff (x + y) = ofCoeff x + ofCoeff y

@[simp]

theorem MonoidAlgebra.coeff_sum {R : Type u_1} {M : Type u_4} {ι : Type u_7} [Semiring R] (s : Finset ι) (f : ι → MonoidAlgebra R M) : (∑ i ∈ s, f i).coeff = ∑ i ∈ s, (f i).coeff

@[simp]

theorem AddMonoidAlgebra.coeff_sum {R : Type u_1} {M : Type u_4} {ι : Type u_7} [Semiring R] (s : Finset ι) (f : ι → AddMonoidAlgebra R M) : (∑ i ∈ s, f i).coeff = ∑ i ∈ s, (f i).coeff

@[simp]

theorem MonoidAlgebra.ofCoeff_sum {R : Type u_1} {M : Type u_4} {ι : Type u_7} [Semiring R] (s : Finset ι) (f : ι → M →₀ R) : ofCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, ofCoeff (f i)

@[simp]

theorem AddMonoidAlgebra.ofCoeff_sum {R : Type u_1} {M : Type u_4} {ι : Type u_7} [Semiring R] (s : Finset ι) (f : ι → M →₀ R) : ofCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, ofCoeff (f i)

@[simp]

theorem MonoidAlgebra.coeff_finsuppSum {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [Semiring R] [AddCommMonoid N] (f : ι →₀ N) (g : ι → N → MonoidAlgebra R M) : (f.sum g).coeff = f.sum fun (i : ι) (n : N) => (g i n).coeff

@[simp]

theorem AddMonoidAlgebra.coeff_finsuppSum {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [Semiring R] [AddCommMonoid N] (f : ι →₀ N) (g : ι → N → AddMonoidAlgebra R M) : (f.sum g).coeff = f.sum fun (i : ι) (n : N) => (g i n).coeff

@[simp]

theorem MonoidAlgebra.ofCoeff_finsuppSum {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [Semiring R] [AddCommMonoid N] (f : ι →₀ N) (g : ι → N → M →₀ R) : ofCoeff (f.sum g) = f.sum fun (i : ι) (n : N) => ofCoeff (g i n)

@[simp]

theorem AddMonoidAlgebra.ofCoeff_finsuppSum {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [Semiring R] [AddCommMonoid N] (f : ι →₀ N) (g : ι → N → M →₀ R) : ofCoeff (f.sum g) = f.sum fun (i : ι) (n : N) => ofCoeff (g i n)

@[reducible, inline]

noncomputable abbrev MonoidAlgebra.single {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) : MonoidAlgebra R M

MonoidAlgebra.single m r for m : M, r : R is the element rm : R[M].

@[reducible, inline]

noncomputable abbrev AddMonoidAlgebra.single {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) : AddMonoidAlgebra R M

AddMonoidAlgebra.single m r for m : M, r : R is the element rm : R[M].

noncomputable def MonoidAlgebra.erase {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (x : MonoidAlgebra R M) : MonoidAlgebra R M

Remove a term from an element of the monoid algebra.

noncomputable def AddMonoidAlgebra.erase {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (x : AddMonoidAlgebra R M) : AddMonoidAlgebra R M

Remove a term from an element of the additive monoid algebra.

@[simp]

theorem MonoidAlgebra.coeff_erase {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (x : MonoidAlgebra R M) : (erase m x).coeff = Finsupp.erase m x.coeff

@[simp]

theorem AddMonoidAlgebra.coeff_erase {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (x : AddMonoidAlgebra R M) : (erase m x).coeff = Finsupp.erase m x.coeff

@[simp]

theorem MonoidAlgebra.ofCoeff_erase {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (x : M →₀ R) : ofCoeff (Finsupp.erase m x) = erase m (ofCoeff x)

@[simp]

theorem AddMonoidAlgebra.ofCoeff_erase {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (x : M →₀ R) : ofCoeff (Finsupp.erase m x) = erase m (ofCoeff x)

@[simp]

theorem MonoidAlgebra.erase_zero {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) : erase m 0 = 0

@[simp]

theorem AddMonoidAlgebra.erase_zero {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) : erase m 0 = 0

@[simp]

theorem MonoidAlgebra.erase_single {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) : erase m (single m r) = 0

@[simp]

theorem AddMonoidAlgebra.erase_single {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) : erase m (single m r) = 0

noncomputable def MonoidAlgebra.update {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) (x : MonoidAlgebra R M) : MonoidAlgebra R M

Replace the m-th coefficient of an element x of the monoid algebra by a given value r : R. If r = 0, this is equal to x.erase m.

noncomputable def AddMonoidAlgebra.update {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) (x : AddMonoidAlgebra R M) : AddMonoidAlgebra R M

Replace the m-th coefficient of an element x of the monoid algebra by a given value r : R. If r = 0, this is equal to x.erase m.

@[simp]

theorem MonoidAlgebra.coeff_update {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) (x : MonoidAlgebra R M) : (update m r x).coeff = x.coeff.update m r

@[simp]

theorem AddMonoidAlgebra.coeff_update {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) (x : AddMonoidAlgebra R M) : (update m r x).coeff = x.coeff.update m r

@[simp]

theorem MonoidAlgebra.ofCoeff_update {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) (x : M →₀ R) : ofCoeff (x.update m r) = update m r (ofCoeff x)

@[simp]

theorem AddMonoidAlgebra.ofCoeff_update {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) (x : M →₀ R) : ofCoeff (x.update m r) = update m r (ofCoeff x)

Basic scalar multiplication instances

This section collects instances needed for the algebraic structure of Polynomial, which is defined in terms of MonoidAlgebra. Further results on scalar multiplication can be found in Mathlib/Algebra/MonoidAlgebra/Module.lean.

@[implicit_reducible]

noncomputable instance MonoidAlgebra.smulZeroClass {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] : SMulZeroClass A (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.smulZeroClass {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] : SMulZeroClass A (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.coeff_smul {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : MonoidAlgebra R M) : (a • x).coeff = a • x.coeff

@[simp]

theorem AddMonoidAlgebra.coeff_smul {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : AddMonoidAlgebra R M) : (a • x).coeff = a • x.coeff

@[simp]

theorem MonoidAlgebra.ofCoeff_smul {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : M →₀ R) : ofCoeff (a • x) = a • ofCoeff x

@[simp]

theorem AddMonoidAlgebra.ofCoeff_smul {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : M →₀ R) : ofCoeff (a • x) = a • ofCoeff x

@[simp]

theorem MonoidAlgebra.smul_apply {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : MonoidAlgebra R M) (m : M) : (a • x) m = a • x m

@[simp]

theorem AddMonoidAlgebra.smul_apply {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : AddMonoidAlgebra R M) (m : M) : (a • x) m = a • x m

@[simp]

theorem MonoidAlgebra.smul_single {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (m : M) (r : R) : a • single m r = single m (a • r)

@[simp]

theorem AddMonoidAlgebra.smul_single {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (m : M) (r : R) : a • single m r = single m (a • r)

theorem MonoidAlgebra.smul_single' {R : Type u_1} {M : Type u_4} [Semiring R] (r' : R) (m : M) (r : R) : r' • single m r = single m (r' * r)

theorem AddMonoidAlgebra.smul_single' {R : Type u_1} {M : Type u_4} [Semiring R] (r' : R) (m : M) (r : R) : r' • single m r = single m (r' * r)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.distribSMul {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [DistribSMul N R] : DistribSMul N (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.distribSMul {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [DistribSMul N R] : DistribSMul N (AddMonoidAlgebra R M)

instance MonoidAlgebra.isScalarTower {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] : IsScalarTower N O (MonoidAlgebra R M)

instance AddMonoidAlgebra.isScalarTower {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] : IsScalarTower N O (AddMonoidAlgebra R M)

instance MonoidAlgebra.smulCommClass {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] : SMulCommClass N O (MonoidAlgebra R M)

instance AddMonoidAlgebra.smulCommClass {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] : SMulCommClass N O (AddMonoidAlgebra R M)

instance MonoidAlgebra.isCentralScalar {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] : IsCentralScalar N (MonoidAlgebra R M)

instance AddMonoidAlgebra.isCentralScalar {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] : IsCentralScalar N (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.coe_add {R : Type u_1} {G : Type u_3} [Semiring R] (f g : MonoidAlgebra R G) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem AddMonoidAlgebra.coe_add {R : Type u_1} {G : Type u_3} [Semiring R] (f g : AddMonoidAlgebra R G) : ⇑(f + g) = ⇑f + ⇑g

theorem MonoidAlgebra.single_zero {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) : single m 0 = 0

theorem AddMonoidAlgebra.single_zero {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) : single m 0 = 0

theorem MonoidAlgebra.single_add {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r₁ r₂ : R) : single m (r₁ + r₂) = single m r₁ + single m r₂

theorem AddMonoidAlgebra.single_add {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r₁ r₂ : R) : single m (r₁ + r₂) = single m r₁ + single m r₂

noncomputable def MonoidAlgebra.singleAddHom {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) : R →+ MonoidAlgebra R M

MonoidAlgebra.single as an AddMonoidHom.

TODO: Rename to singleAddMonoidHom.

noncomputable def AddMonoidAlgebra.singleAddHom {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) : R →+ AddMonoidAlgebra R M

AddMonoidAlgebra.single as an AddMonoidHom.

TODO: Rename to singleAddMonoidHom.

@[simp]

theorem AddMonoidAlgebra.singleAddHom_apply {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) : (singleAddHom m) r = single m r

@[simp]

theorem MonoidAlgebra.singleAddHom_apply {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) : (singleAddHom m) r = single m r

theorem MonoidAlgebra.addHom_ext' {R : Type u_1} {M : Type u_4} [Semiring R] {N : Type u_8} [AddZeroClass N] ⦃f g : MonoidAlgebra R M →+ N⦄ (hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)) : f = g

If two additive homomorphisms from R[M] are equal on each single r m, then they are equal.

We formulate this using equality of AddMonoidHoms so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is ℕ or ℤ, then it suffices to verify f (single a 1) = g (single a 1).

TODO: Rename to addMonoidHom_ext'.

theorem AddMonoidAlgebra.addHom_ext' {R : Type u_1} {M : Type u_4} [Semiring R] {N : Type u_8} [AddZeroClass N] ⦃f g : AddMonoidAlgebra R M →+ N⦄ (hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)) : f = g

If two additive homomorphisms from R[M] are equal on each single r m, then they are equal.

We formulate this using equality of AddMonoidHoms so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is ℕ or ℤ, then it suffices to verify f (single a 1) = g (single a 1).

TODO: Rename to addMonoidHom_ext'.

theorem AddMonoidAlgebra.addHom_ext'_iff {R : Type u_1} {M : Type u_4} [Semiring R] {N : Type u_8} [AddZeroClass N] {f g : AddMonoidAlgebra R M →+ N} : f = g ↔ ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)

theorem MonoidAlgebra.addHom_ext'_iff {R : Type u_1} {M : Type u_4} [Semiring R] {N : Type u_8} [AddZeroClass N] {f g : MonoidAlgebra R M →+ N} : f = g ↔ ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)

theorem MonoidAlgebra.sum_single_index {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] {m : M} {r : R} {h : M → R → N} (h_zero : h m 0 = 0) : Finsupp.sum (single m r) h = h m r

theorem AddMonoidAlgebra.sum_single_index {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] {m : M} {r : R} {h : M → R → N} (h_zero : h m 0 = 0) : Finsupp.sum (single m r) h = h m r

@[simp]

theorem MonoidAlgebra.sum_single {R : Type u_1} {M : Type u_4} [Semiring R] (x : MonoidAlgebra R M) : Finsupp.sum x single = x

@[simp]

theorem AddMonoidAlgebra.sum_single {R : Type u_1} {M : Type u_4} [Semiring R] (x : AddMonoidAlgebra R M) : Finsupp.sum x single = x

theorem MonoidAlgebra.single_apply {R : Type u_1} {M : Type u_4} [Semiring R] {a a' : M} {b : R} [Decidable (a = a')] : (single a b) a' = if a = a' then b else 0

theorem AddMonoidAlgebra.single_apply {R : Type u_1} {M : Type u_4} [Semiring R] {a a' : M} {b : R} [Decidable (a = a')] : (single a b) a' = if a = a' then b else 0

@[simp]

theorem MonoidAlgebra.single_eq_zero {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m : M} : single m r = 0 ↔ r = 0

@[simp]

theorem AddMonoidAlgebra.single_eq_zero {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m : M} : single m r = 0 ↔ r = 0

theorem MonoidAlgebra.single_ne_zero {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m : M} : single m r ≠ 0 ↔ r ≠ 0

theorem AddMonoidAlgebra.single_ne_zero {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m : M} : single m r ≠ 0 ↔ r ≠ 0

theorem MonoidAlgebra.induction_linear {R : Type u_1} {M : Type u_4} [Semiring R] {p : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (zero : p 0) (add : ∀ (x y : MonoidAlgebra R M), p x → p y → p (x + y)) (single : ∀ (m : M) (r : R), p (single m r)) : p x

theorem AddMonoidAlgebra.induction_linear {R : Type u_1} {M : Type u_4} [Semiring R] {p : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M) (zero : p 0) (add : ∀ (x y : AddMonoidAlgebra R M), p x → p y → p (x + y)) (single : ∀ (m : M) (r : R), p (single m r)) : p x

@[implicit_reducible]

noncomputable instance MonoidAlgebra.one {R : Type u_1} {M : Type u_4} [Semiring R] [One M] : One (MonoidAlgebra R M)

The unit of the multiplication is single 1 1, i.e. the function that is 1 at 1 and 0 elsewhere.

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.zero {R : Type u_1} {M : Type u_4} [Semiring R] [Zero M] : One (AddMonoidAlgebra R M)

The unit of the multiplication is single 1 1, i.e. the function that is 1 at 1 and 0 elsewhere.

theorem MonoidAlgebra.one_def {R : Type u_1} {M : Type u_4} [Semiring R] [One M] : 1 = single 1 1

theorem AddMonoidAlgebra.one_def {R : Type u_1} {M : Type u_4} [Semiring R] [Zero M] : 1 = single 0 1

@[irreducible]

noncomputable def MonoidAlgebra.mul' {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] (x y : MonoidAlgebra R M) : MonoidAlgebra R M

The multiplication in a monoid algebra.

We make it irreducible so that Lean doesn't unfold it when trying to unify two different things.

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.instMul {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] : Mul (AddMonoidAlgebra R M)

The product of f g : k[G] is the finitely supported function whose value at a is the sum of f x * g y over all pairs x, y such that x + y = a. (Think of the product of multivariate polynomials where α is the additive monoid of monomial exponents.)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.instMul {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] : Mul (MonoidAlgebra R M)

The product of x y : R[M] is the finitely supported function whose value at m is the sum of x m₁ * y m₂ over all pairs m₁, m₂ such that m₁ * m₂ = m.

(Think of the group ring of a group.)

theorem MonoidAlgebra.mul_def {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] (x y : MonoidAlgebra R M) : x * y = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => single (m₁ * m₂) (r₁ * r₂)

theorem AddMonoidAlgebra.mul_def {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] (x y : AddMonoidAlgebra R M) : x * y = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => single (m₁ + m₂) (r₁ * r₂)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonUnitalNonAssocSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] : NonUnitalNonAssocSemiring (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonUnitalNonAssocSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] : NonUnitalNonAssocSemiring (AddMonoidAlgebra R M)

theorem MonoidAlgebra.mul_apply {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] [DecidableEq M] (x y : MonoidAlgebra R M) (m : M) : (x * y) m = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => if m₁ * m₂ = m then r₁ * r₂ else 0

theorem AddMonoidAlgebra.mul_apply {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] [DecidableEq M] (x y : AddMonoidAlgebra R M) (m : M) : (x * y) m = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => if m₁ + m₂ = m then r₁ * r₂ else 0

theorem MonoidAlgebra.mul_apply_antidiagonal {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] (x y : MonoidAlgebra R M) (m : M) (s : Finset (M × M)) (hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m) : (x * y) m = ∑ p ∈ s, x p.1 * y p.2

theorem AddMonoidAlgebra.mul_apply_antidiagonal {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] (x y : AddMonoidAlgebra R M) (m : M) (s : Finset (M × M)) (hs : ∀ {p : M × M}, p ∈ s ↔ p.1 + p.2 = m) : (x * y) m = ∑ p ∈ s, x p.1 * y p.2

@[simp]

theorem MonoidAlgebra.single_mul_single {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] (m₁ m₂ : M) (r₁ r₂ : R) : single m₁ r₁ * single m₂ r₂ = single (m₁ * m₂) (r₁ * r₂)

@[simp]

theorem AddMonoidAlgebra.single_mul_single {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] (m₁ m₂ : M) (r₁ r₂ : R) : single m₁ r₁ * single m₂ r₂ = single (m₁ + m₂) (r₁ * r₂)

@[simp]

theorem MonoidAlgebra.single_commute_single {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} [Mul M] (hm : Commute m₁ m₂) (hr : Commute r₁ r₂) : Commute (single m₁ r₁) (single m₂ r₂)

@[simp]

theorem AddMonoidAlgebra.single_commute_single {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} [Add M] (hm : AddCommute m₁ m₂) (hr : Commute r₁ r₂) : Commute (single m₁ r₁) (single m₂ r₂)

@[simp]

theorem MonoidAlgebra.single_commute {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m : M} [Mul M] (hm : ∀ (m' : M), Commute m m') (hr : ∀ (r' : R), Commute r r') (x : MonoidAlgebra R M) : Commute (single m r) x

@[simp]

theorem AddMonoidAlgebra.single_commute {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m : M} [Add M] (hm : ∀ (m' : M), AddCommute m m') (hr : ∀ (r' : R), Commute r r') (x : AddMonoidAlgebra R M) : Commute (single m r) x

theorem MonoidAlgebra.mul_single_apply_aux {R : Type u_1} {M : Type u_4} [Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Mul M] (H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂) : (x * single m r) m₁ = x m₂ * r

theorem AddMonoidAlgebra.mul_single_apply_aux {R : Type u_1} {M : Type u_4} [Semiring R] {x : AddMonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Add M] (H : ∀ m' ∈ x.support, m' + m = m₁ ↔ m' = m₂) : (x * single m r) m₁ = x m₂ * r

theorem MonoidAlgebra.single_mul_apply_aux {R : Type u_1} {M : Type u_4} [Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Mul M] (H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂) : (single m r * x) m₁ = r * x m₂

theorem AddMonoidAlgebra.single_mul_apply_aux {R : Type u_1} {M : Type u_4} [Semiring R] {x : AddMonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Add M] (H : ∀ m' ∈ x.support, m + m' = m₁ ↔ m' = m₂) : (single m r * x) m₁ = r * x m₂

@[simp]

theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul {R : Type u_1} {M : Type u_4} [Semiring R] {m m' : M} [Mul M] (r : R) (x : MonoidAlgebra R M) (h : ¬∃ (d : M), m' = d * m) : (x * single m r) m' = 0

@[simp]

theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add {R : Type u_1} {M : Type u_4} [Semiring R] {m m' : M} [Add M] (r : R) (x : AddMonoidAlgebra R M) (h : ¬∃ (d : M), m' = d + m) : (x * single m r) m' = 0

@[simp]

theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul {R : Type u_1} {M : Type u_4} [Semiring R] {m m' : M} [Mul M] (r : R) (x : MonoidAlgebra R M) (h : ¬∃ (d : M), m' = m * d) : (single m r * x) m' = 0

@[simp]

theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add {R : Type u_1} {M : Type u_4} [Semiring R] {m m' : M} [Add M] (r : R) (x : AddMonoidAlgebra R M) (h : ¬∃ (d : M), m' = m + d) : (single m r * x) m' = 0

noncomputable def MonoidAlgebra.ofMagma (R : Type u_8) (M : Type u_9) [Semiring R] [Mul M] : M →ₙ* MonoidAlgebra R M

The embedding of a magma into its magma algebra.

@[simp]

theorem MonoidAlgebra.ofMagma_apply (R : Type u_8) (M : Type u_9) [Semiring R] [Mul M] (a : M) : (ofMagma R M) a = single a 1

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonUnitalSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [Semigroup M] : NonUnitalSemiring (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonUnitalSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [AddSemigroup M] : NonUnitalSemiring (AddMonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonAssocSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] : NonAssocSemiring (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonAssocSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] : NonAssocSemiring (AddMonoidAlgebra R M)

theorem MonoidAlgebra.natCast_def {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] (n : ℕ) : ↑n = single 1 ↑n

theorem AddMonoidAlgebra.natCast_def {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (n : ℕ) : ↑n = single 0 ↑n

theorem MonoidAlgebra.mul_single_one_apply {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M) : (x * single 1 r) m = x m * r

theorem AddMonoidAlgebra.mul_single_zero_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (x : AddMonoidAlgebra R M) (r : R) (m : M) : (x * single 0 r) m = x m * r

theorem MonoidAlgebra.single_one_mul_apply {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M) : (single 1 r * x) m = r * x m

theorem AddMonoidAlgebra.single_zero_mul_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (x : AddMonoidAlgebra R M) (r : R) (m : M) : (single 0 r * x) m = r * x m

noncomputable def MonoidAlgebra.of (R : Type u_8) (M : Type u_9) [Semiring R] [MulOneClass M] : M →* MonoidAlgebra R M

The embedding of a unital magma into its magma algebra.

@[simp]

theorem MonoidAlgebra.of_apply (R : Type u_8) (M : Type u_9) [Semiring R] [MulOneClass M] (m : M) : (of R M) m = single m 1

theorem MonoidAlgebra.of_injective {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] [Nontrivial R] : Function.Injective ⇑(of R M)

theorem MonoidAlgebra.of_commute {R : Type u_1} {M : Type u_4} [Semiring R] {m : M} [MulOneClass M] (h : ∀ (m' : M), Commute m m') (f : MonoidAlgebra R M) : Commute ((of R M) m) f

noncomputable def MonoidAlgebra.singleHom {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] : R × M →* MonoidAlgebra R M

MonoidAlgebra.single as a MonoidHom from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of MonoidAlgebra.single.

@[simp]

theorem MonoidAlgebra.singleHom_apply {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] (a : R × M) : singleHom a = single a.2 a.1

noncomputable def MonoidAlgebra.singleOneRingHom {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] : R →+* MonoidAlgebra R M

MonoidAlgebra.single 1 as a RingHom

noncomputable def AddMonoidAlgebra.singleZeroRingHom {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] : R →+* AddMonoidAlgebra R M

AddMonoidAlgebra.single 1 as a RingHom

@[simp]

theorem MonoidAlgebra.singleOneRingHom_apply {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] (a✝ : R) : singleOneRingHom a✝ = (↑(singleAddHom 1)).toFun a✝

@[simp]

theorem AddMonoidAlgebra.singleZeroRingHom_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (a✝ : R) : singleZeroRingHom a✝ = (↑(singleAddHom 0)).toFun a✝

theorem MonoidAlgebra.ringHom_ext {R : Type u_1} {S : Type u_2} {M : Type u_4} [Semiring R] [MulOneClass M] [Semiring S] {f g : MonoidAlgebra R M →+* S} (h₁ : ∀ (r : R), f (single 1 r) = g (single 1 r)) (h_of : ∀ (m : M), f (single m 1) = g (single m 1)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 1 r, then they are equal.

theorem AddMonoidAlgebra.ringHom_ext {R : Type u_1} {S : Type u_2} {M : Type u_4} [Semiring R] [AddZeroClass M] [Semiring S] {f g : AddMonoidAlgebra R M →+* S} (h₁ : ∀ (r : R), f (single 0 r) = g (single 0 r)) (h_of : ∀ (m : M), f (single m 1) = g (single m 1)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 0 r, then they are equal.

theorem MonoidAlgebra.ringHom_ext' {R : Type u_1} {S : Type u_2} {M : Type u_4} [Semiring R] [MulOneClass M] [Semiring S] {f g : MonoidAlgebra R M →+* S} (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom) (h_of : (↑f).comp (of R M) = (↑g).comp (of R M)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 1 r, then they are equal.

See note [partially-applied ext lemmas].

theorem MonoidAlgebra.ringHom_ext'_iff {R : Type u_1} {S : Type u_2} {M : Type u_4} [Semiring R] [MulOneClass M] [Semiring S] {f g : MonoidAlgebra R M →+* S} : f = g ↔ f.comp singleOneRingHom = g.comp singleOneRingHom ∧ (↑f).comp (of R M) = (↑g).comp (of R M)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.semiring {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] : Semiring (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.semiring {R : Type u_1} {M : Type u_4} [Semiring R] [AddMonoid M] : Semiring (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.single_pow {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] (m : M) (r : R) (n : ℕ) : single m r ^ n = single (m ^ n) (r ^ n)

@[simp]

theorem AddMonoidAlgebra.single_pow {R : Type u_1} {M : Type u_4} [Semiring R] [AddMonoid M] (m : M) (r : R) (n : ℕ) : single m r ^ n = single (n • m) (r ^ n)

theorem MonoidAlgebra.induction_on {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] {p : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (hM : ∀ (m : M), p ((of R M) m)) (hadd : ∀ (x y : MonoidAlgebra R M), p x → p y → p (x + y)) (hsmul : ∀ (r : R) (x : MonoidAlgebra R M), p x → p (r • x)) : p x

instance MonoidAlgebra.isLocalHom_singleOneRingHom {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] : IsLocalHom singleOneRingHom

instance AddMonoidAlgebra.isLocalHom_singleZeroRingHom {R : Type u_1} {M : Type u_4} [Semiring R] [AddMonoid M] : IsLocalHom singleZeroRingHom

noncomputable def MonoidAlgebra.uniqueRingEquiv {R : Type u_1} (M : Type u_4) [Semiring R] [Monoid M] [Unique M] : MonoidAlgebra R M ≃+* R

The trivial monoid algebra is the base ring.

noncomputable def AddMonoidAlgebra.uniqueRingEquiv {R : Type u_1} (M : Type u_4) [Semiring R] [AddMonoid M] [Unique M] : AddMonoidAlgebra R M ≃+* R

The trivial additive monoid algebra is the base ring.

@[simp]

theorem AddMonoidAlgebra.uniqueRingEquiv_apply {R : Type u_1} (M : Type u_4) [Semiring R] [AddMonoid M] [Unique M] (a✝ : M →₀ R) : (uniqueRingEquiv M) a✝ = a✝ default

@[simp]

theorem MonoidAlgebra.uniqueRingEquiv_apply {R : Type u_1} (M : Type u_4) [Semiring R] [Monoid M] [Unique M] (a✝ : M →₀ R) : (uniqueRingEquiv M) a✝ = a✝ default

@[simp]

theorem AddMonoidAlgebra.uniqueRingEquiv_symm_apply {R : Type u_1} (M : Type u_4) [Semiring R] [AddMonoid M] [Unique M] (a✝ : R) : (uniqueRingEquiv M).symm a✝ = Finsupp.equivFunOnFinite.symm (uniqueElim a✝)

@[simp]

theorem MonoidAlgebra.uniqueRingEquiv_symm_apply {R : Type u_1} (M : Type u_4) [Semiring R] [Monoid M] [Unique M] (a✝ : R) : (uniqueRingEquiv M).symm a✝ = Finsupp.equivFunOnFinite.symm (uniqueElim a✝)

noncomputable def MonoidAlgebra.curryRingEquiv {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [Monoid M] [Monoid N] : MonoidAlgebra R (M × N) ≃+* MonoidAlgebra (MonoidAlgebra R N) M

A product monoid algebra is a nested monoid algebra.

noncomputable def AddMonoidAlgebra.curryRingEquiv {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddMonoid M] [AddMonoid N] : AddMonoidAlgebra R (M × N) ≃+* AddMonoidAlgebra (AddMonoidAlgebra R N) M

An additive product monoid algebra is a nested additive monoid algebra.

@[simp]

theorem MonoidAlgebra.curryRingEquiv_single {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [Monoid M] [Monoid N] (m : M) (n : N) (r : R) : curryRingEquiv (single (m, n) r) = single m (single n r)

@[simp]

theorem AddMonoidAlgebra.curryRingEquiv_single {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddMonoid M] [AddMonoid N] (m : M) (n : N) (r : R) : curryRingEquiv (single (m, n) r) = single m (single n r)

@[simp]

theorem MonoidAlgebra.curryRingEquiv_symm_single {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [Monoid M] [Monoid N] (m : M) (n : N) (r : R) : curryRingEquiv.symm (single m (single n r)) = single (m, n) r

@[simp]

theorem AddMonoidAlgebra.curryRingEquiv_symm_single {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddMonoid M] [AddMonoid N] (m : M) (n : N) (r : R) : curryRingEquiv.symm (single m (single n r)) = single (m, n) r

@[simp]

theorem MonoidAlgebra.mul_single_apply {R : Type u_1} {G : Type u_3} [Semiring R] [Group G] (x : MonoidAlgebra R G) (r : R) (g h : G) : (x * single g r) h = x (h * g⁻¹) * r

@[simp]

theorem AddMonoidAlgebra.mul_single_apply {R : Type u_1} {G : Type u_3} [Semiring R] [AddGroup G] (x : AddMonoidAlgebra R G) (r : R) (g h : G) : (x * single g r) h = x (h + -g) * r

@[simp]

theorem MonoidAlgebra.single_mul_apply {R : Type u_1} {G : Type u_3} [Semiring R] [Group G] (x : MonoidAlgebra R G) (r : R) (g h : G) : (single g r * x) h = r * x (g⁻¹ * h)

@[simp]

theorem AddMonoidAlgebra.single_mul_apply {R : Type u_1} {G : Type u_3} [Semiring R] [AddGroup G] (x : AddMonoidAlgebra R G) (r : R) (g h : G) : (single g r * x) h = r * x (-g + h)

theorem MonoidAlgebra.mul_apply_left {R : Type u_1} {G : Type u_3} [Semiring R] [Group G] (x y : MonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum x fun (h : G) (r : R) => r * y (h⁻¹ * g)

theorem AddMonoidAlgebra.mul_apply_left {R : Type u_1} {G : Type u_3} [Semiring R] [AddGroup G] (x y : AddMonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum x fun (h : G) (r : R) => r * y (-h + g)

theorem MonoidAlgebra.mul_apply_right {R : Type u_1} {G : Type u_3} [Semiring R] [Group G] (x y : MonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum y fun (h : G) (r : R) => x (g * h⁻¹) * r

theorem AddMonoidAlgebra.mul_apply_right {R : Type u_1} {G : Type u_3} [Semiring R] [AddGroup G] (x y : AddMonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum y fun (h : G) (r : R) => x (g + -h) * r

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonUnitalCommSemiring {R : Type u_1} {M : Type u_4} [CommSemiring R] [CommSemigroup M] : NonUnitalCommSemiring (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonUnitalCommSemiring {R : Type u_1} {M : Type u_4} [CommSemiring R] [AddCommSemigroup M] : NonUnitalCommSemiring (AddMonoidAlgebra R M)

theorem MonoidAlgebra.single_one_comm {R : Type u_1} {M : Type u_4} [CommSemiring R] [MulOneClass M] (r : R) (f : MonoidAlgebra R M) : single 1 r * f = f * single 1 r

theorem AddMonoidAlgebra.single_zero_comm {R : Type u_1} {M : Type u_4} [CommSemiring R] [AddZeroClass M] (r : R) (f : AddMonoidAlgebra R M) : single 0 r * f = f * single 0 r

@[implicit_reducible]

noncomputable instance MonoidAlgebra.commSemiring {R : Type u_1} {M : Type u_4} [CommSemiring R] [CommMonoid M] : CommSemiring (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.commSemiring {R : Type u_1} {M : Type u_4} [CommSemiring R] [AddCommMonoid M] : CommSemiring (AddMonoidAlgebra R M)

theorem MonoidAlgebra.prod_single {R : Type u_1} {M : Type u_4} {ι : Type u_7} [CommSemiring R] [CommMonoid M] (s : Finset ι) (m : ι → M) (r : ι → R) : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)

theorem AddMonoidAlgebra.prod_single {R : Type u_1} {M : Type u_4} {ι : Type u_7} [CommSemiring R] [AddCommMonoid M] (s : Finset ι) (m : ι → M) (r : ι → R) : ∏ i ∈ s, single (m i) (r i) = single (∑ i ∈ s, m i) (∏ i ∈ s, r i)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.addCommGroup {R : Type u_1} {M : Type u_4} [Ring R] : AddCommGroup (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.addAddCommGroup {R : Type u_1} {M : Type u_4} [Ring R] : AddCommGroup (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.coeff_neg {R : Type u_1} {M : Type u_4} [Ring R] (x : MonoidAlgebra R M) : (-x).coeff = -x.coeff

@[simp]

theorem AddMonoidAlgebra.coeff_neg {R : Type u_1} {M : Type u_4} [Ring R] (x : AddMonoidAlgebra R M) : (-x).coeff = -x.coeff

@[simp]

theorem MonoidAlgebra.ofCoeff_neg {R : Type u_1} {M : Type u_4} [Ring R] (x : M →₀ R) : ofCoeff (-x) = -ofCoeff x

@[simp]

theorem AddMonoidAlgebra.ofCoeff_neg {R : Type u_1} {M : Type u_4} [Ring R] (x : M →₀ R) : ofCoeff (-x) = -ofCoeff x

@[simp]

theorem MonoidAlgebra.coeff_sub {R : Type u_1} {M : Type u_4} [Ring R] (x y : MonoidAlgebra R M) : (x - y).coeff = x.coeff - y.coeff

@[simp]

theorem AddMonoidAlgebra.coeff_sub {R : Type u_1} {M : Type u_4} [Ring R] (x y : AddMonoidAlgebra R M) : (x - y).coeff = x.coeff - y.coeff

@[simp]

theorem MonoidAlgebra.ofCoeff_sub {R : Type u_1} {M : Type u_4} [Ring R] (x y : M →₀ R) : ofCoeff (x - y) = ofCoeff x - ofCoeff y

@[simp]

theorem AddMonoidAlgebra.ofCoeff_sub {R : Type u_1} {M : Type u_4} [Ring R] (x y : M →₀ R) : ofCoeff (x - y) = ofCoeff x - ofCoeff y

@[simp]

theorem MonoidAlgebra.neg_apply {R : Type u_1} {M : Type u_4} [Ring R] (m : M) (x : MonoidAlgebra R M) : (-x) m = -x m

@[simp]

theorem AddMonoidAlgebra.neg_apply {R : Type u_1} {M : Type u_4} [Ring R] (m : M) (x : AddMonoidAlgebra R M) : (-x) m = -x m

theorem MonoidAlgebra.single_neg {R : Type u_1} {M : Type u_4} [Ring R] (m : M) (r : R) : single m (-r) = -single m r

theorem AddMonoidAlgebra.single_neg {R : Type u_1} {M : Type u_4} [Ring R] (m : M) (r : R) : single m (-r) = -single m r

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonUnitalNonAssocRing {R : Type u_1} {M : Type u_4} [Ring R] [Mul M] : NonUnitalNonAssocRing (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonUnitalNonAssocRing {R : Type u_1} {M : Type u_4} [Ring R] [Add M] : NonUnitalNonAssocRing (AddMonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonUnitalRing {R : Type u_1} {M : Type u_4} [Ring R] [Semigroup M] : NonUnitalRing (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonUnitalRing {R : Type u_1} {M : Type u_4} [Ring R] [AddSemigroup M] : NonUnitalRing (AddMonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonAssocRing {R : Type u_1} {M : Type u_4} [Ring R] [MulOneClass M] : NonAssocRing (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonAssocRing {R : Type u_1} {M : Type u_4} [Ring R] [AddZeroClass M] : NonAssocRing (AddMonoidAlgebra R M)

theorem MonoidAlgebra.intCast_def {R : Type u_1} {M : Type u_4} [Ring R] [MulOneClass M] (z : ℤ) : ↑z = single 1 ↑z

theorem AddMonoidAlgebra.intCast_def {R : Type u_1} {M : Type u_4} [Ring R] [AddZeroClass M] (z : ℤ) : ↑z = single 0 ↑z

@[implicit_reducible]

noncomputable instance MonoidAlgebra.ring {R : Type u_1} {M : Type u_4} [Ring R] [Monoid M] : Ring (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.ring {R : Type u_1} {M : Type u_4} [Ring R] [AddMonoid M] : Ring (AddMonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.nonUnitalCommRing {R : Type u_1} {M : Type u_4} [CommRing R] [CommSemigroup M] : NonUnitalCommRing (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.nonUnitalCommRing {R : Type u_1} {M : Type u_4} [CommRing R] [AddCommSemigroup M] : NonUnitalCommRing (AddMonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance MonoidAlgebra.commRing {R : Type u_1} {M : Type u_4} [CommRing R] [CommMonoid M] : CommRing (MonoidAlgebra R M)

@[implicit_reducible]

noncomputable instance AddMonoidAlgebra.commRing {R : Type u_1} {M : Type u_4} [CommRing R] [AddCommMonoid M] : CommRing (AddMonoidAlgebra R M)

Additive monoids

noncomputable def AddMonoidAlgebra.ofMagma (R : Type u_8) (M : Type u_9) [Semiring R] [Add M] : Multiplicative M →ₙ* AddMonoidAlgebra R M

The embedding of an additive magma into its additive magma algebra.

@[simp]

theorem AddMonoidAlgebra.ofMagma_apply (R : Type u_8) (M : Type u_9) [Semiring R] [Add M] (a : Multiplicative M) : (ofMagma R M) a = single (Multiplicative.toAdd a) 1

noncomputable def AddMonoidAlgebra.of (R : Type u_8) (M : Type u_9) [Semiring R] [AddZeroClass M] : Multiplicative M →* AddMonoidAlgebra R M

Embedding of a magma with zero into its magma algebra.

noncomputable def AddMonoidAlgebra.of' (R : Type u_8) (M : Type u_9) [Semiring R] : M → AddMonoidAlgebra R M

Embedding of a magma with zero M, into its magma algebra, having M as source.

@[simp]

theorem AddMonoidAlgebra.of_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (a : Multiplicative M) : (of R M) a = single (Multiplicative.toAdd a) 1

@[simp]

theorem AddMonoidAlgebra.of'_apply {R : Type u_1} {M : Type u_4} [Semiring R] (a : M) : of' R M a = single a 1

theorem AddMonoidAlgebra.of'_eq_of {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (a : M) : of' R M a = (of R M) (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.of_injective {R : Type u_1} {M : Type u_4} [Semiring R] [Nontrivial R] [AddZeroClass M] : Function.Injective ⇑(of R M)

theorem AddMonoidAlgebra.of'_commute {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] {a : M} (h : ∀ (a' : M), AddCommute a a') (f : AddMonoidAlgebra R M) : Commute (of' R M a) f

noncomputable def AddMonoidAlgebra.singleHom {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] : R × Multiplicative M →* AddMonoidAlgebra R M

Finsupp.single as a MonoidHom from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of Finsupp.single.

@[simp]

theorem AddMonoidAlgebra.singleHom_apply {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (a : R × Multiplicative M) : singleHom a = single (Multiplicative.toAdd a.2) a.1

theorem AddMonoidAlgebra.induction_on {R : Type u_1} {M : Type u_4} [Semiring R] [AddMonoid M] {p : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M) (hM : ∀ (m : M), p ((of R M) (Multiplicative.ofAdd m))) (hadd : ∀ (x y : AddMonoidAlgebra R M), p x → p y → p (x + y)) (hsmul : ∀ (r : R) (x : AddMonoidAlgebra R M), p x → p (r • x)) : p x

theorem AddMonoidAlgebra.ringHom_ext' {R : Type u_1} {S : Type u_2} {M : Type u_4} [Semiring R] [Semiring S] [AddMonoid M] {f g : AddMonoidAlgebra R M →+* S} (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom) (h_of : (↑f).comp (of R M) = (↑g).comp (of R M)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 0 r, then they are equal.

See note [partially-applied ext lemmas].

theorem AddMonoidAlgebra.ringHom_ext'_iff {R : Type u_1} {S : Type u_2} {M : Type u_4} [Semiring R] [Semiring S] [AddMonoid M] {f g : AddMonoidAlgebra R M →+* S} : f = g ↔ f.comp singleZeroRingHom = g.comp singleZeroRingHom ∧ (↑f).comp (of R M) = (↑g).comp (of R M)