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 and AddMonoidAlgebra R M as one-field structures around M →₀ R, and then define the convolution product on these.

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

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

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

structure 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.

• ofCoeff :: (
• coeff : M →₀ R

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

• )

structure 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.

• ofCoeff :: (
• coeff : M →₀ R

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

• )

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 AddMonoidAlgebra.delabOfCoeff : Lean.PrettyPrinter.Delaborator.Delab

This prevents ofCoeff x being printed as { coeff := x } by delabStructureInstance.

def MonoidAlgebra.delabOfCoeff : Lean.PrettyPrinter.Delaborator.Delab

This prevents ofCoeff x being printed as { coeff := x } by delabStructureInstance.

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.

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

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

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

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 AddMonoidAlgebra.coeffEquiv_symm_apply {R : Type u_1} {M : Type u_4} [Semiring R] (coeff : M →₀ R) : coeffEquiv.symm coeff = ofCoeff coeff

@[simp]

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

@[simp]

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

@[simp]

theorem MonoidAlgebra.coeffEquiv_apply {R : Type u_1} {M : Type u_4} [Semiring R] (self : MonoidAlgebra R M) : coeffEquiv self = self.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

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

Alias of the forward direction of MonoidAlgebra.coeff_inj.

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

Alias of the forward direction of AddMonoidAlgebra.coeff_inj.

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

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

@[instance_reducible]

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

@[instance_reducible]

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

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

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

noncomputable instance AddMonoidAlgebra.instAddCommMonoid {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)

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] (coeff : M →₀ R) : coeffAddEquiv.symm coeff = ofCoeff coeff

@[simp]

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

@[simp]

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

@[simp]

theorem MonoidAlgebra.coeffAddEquiv_symm_apply {R : Type u_1} {M : Type u_4} [Semiring R] (coeff : M →₀ R) : coeffAddEquiv.symm coeff = ofCoeff 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)

noncomputable def 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].

noncomputable def 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].

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem MonoidAlgebra.single_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} : single m₁ r₁ = single m₂ r₂ ↔ m₁ = m₂ ∧ r₁ = r₂ ∨ r₁ = 0 ∧ r₂ = 0

theorem AddMonoidAlgebra.single_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} : single m₁ r₁ = single m₂ r₂ ↔ m₁ = m₂ ∧ r₁ = r₂ ∨ r₁ = 0 ∧ r₂ = 0

theorem MonoidAlgebra.single_left_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m₁ m₂ : M} (hr : r ≠ 0) : single m₁ r = single m₂ r ↔ m₁ = m₂

theorem AddMonoidAlgebra.single_left_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} {m₁ m₂ : M} (hr : r ≠ 0) : single m₁ r = single m₂ r ↔ m₁ = m₂

@[simp]

theorem MonoidAlgebra.single_right_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m : M} : single m r₁ = single m r₂ ↔ r₁ = r₂

@[simp]

theorem AddMonoidAlgebra.single_right_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m : M} : single m r₁ = single m r₂ ↔ r₁ = r₂

theorem MonoidAlgebra.single_left_injective {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} (hr : r ≠ 0) : Function.Injective fun (m : M) => single m r

MonoidAlgebra.single m r is injective in m if r ≠ 0. For injectivity in r, see MonoidAlgebra.single_injective.

theorem AddMonoidAlgebra.single_left_injective {R : Type u_1} {M : Type u_4} [Semiring R] {r : R} (hr : r ≠ 0) : Function.Injective fun (m : M) => single m r

AddMonoidAlgebra.single m r is injective in m if r ≠ 0. For injectivity in r, see AddMonoidAlgebra.single_injective.

theorem MonoidAlgebra.single_right_injective {R : Type u_1} {M : Type u_4} [Semiring R] {m : M} : Function.Injective (single m)

theorem AddMonoidAlgebra.single_right_injective {R : Type u_1} {M : Type u_4} [Semiring R] {m : M} : Function.Injective (single m)

theorem MonoidAlgebra.single_add_single_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m₁ m₂ m₁' m₂' : M} (hr₁ : r₁ ≠ 0) (hr₂ : r₂ ≠ 0) : single m₁ r₁ + single m₂ r₂ = single m₁' r₁ + single m₂' r₂ ↔ m₁ = m₁' ∧ m₂ = m₂' ∨ r₁ = r₂ ∧ m₁ = m₂' ∧ m₂ = m₁' ∨ r₁ + r₂ = 0 ∧ m₁ = m₂ ∧ m₁' = m₂'

theorem AddMonoidAlgebra.single_add_single_inj {R : Type u_1} {M : Type u_4} [Semiring R] {r₁ r₂ : R} {m₁ m₂ m₁' m₂' : M} (hr₁ : r₁ ≠ 0) (hr₂ : r₂ ≠ 0) : single m₁ r₁ + single m₂ r₂ = single m₁' r₁ + single m₂' r₂ ↔ m₁ = m₁' ∧ m₂ = m₂' ∨ r₁ = r₂ ∧ m₁ = m₂' ∧ m₂ = m₁' ∨ r₁ + r₂ = 0 ∧ m₁ = m₂ ∧ m₁' = 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.

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

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

theorem MonoidAlgebra.coeff_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).coeff m = a • x.coeff m

theorem AddMonoidAlgebra.coeff_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).coeff m = a • x.coeff m

@[deprecated MonoidAlgebra.coeff_smul_apply (since := "2026-06-18")]

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).coeff m = a • x.coeff m

Alias of MonoidAlgebra.coeff_smul_apply.

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

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

@[instance_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.single_zero {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) : single m 0 = 0

@[simp]

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

@[simp]

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₂

@[simp]

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₂

@[deprecated MonoidAlgebra.coeff_add (since := "2026-06-18")]

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

@[deprecated AddMonoidAlgebra.coeff_add (since := "2026-06-18")]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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 MonoidAlgebra.singleAddHom_apply {R : Type u_1} {M : Type u_4} [Semiring R] (m : M) (r : R) : (singleAddHom m) r = single m r

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

theorem MonoidAlgebra.addMonoidHom_ext {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddZeroClass N] ⦃f g : MonoidAlgebra R M →+ N⦄ (h : ∀ (m : M) (r : R), f (single m r) = g (single m r)) : f = g

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

theorem AddMonoidAlgebra.addMonoidHom_ext {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [AddZeroClass N] ⦃f g : AddMonoidAlgebra R M →+ N⦄ (h : ∀ (m : M) (r : R), f (single m r) = g (single m r)) : f = g

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

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)

@[deprecated Finsupp.sum_single_index (since := "2026-06-18")]

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) : (single m r).coeff.sum h = h m r

@[deprecated Finsupp.sum_single_index (since := "2026-06-18")]

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) : (single m r).coeff.sum h = h m r

@[simp]

theorem MonoidAlgebra.sum_coeff_single {R : Type u_1} {M : Type u_4} [Semiring R] (f : MonoidAlgebra R M) : f.coeff.sum single = f

@[simp]

theorem AddMonoidAlgebra.sum_coeff_single {R : Type u_1} {M : Type u_4} [Semiring R] (f : AddMonoidAlgebra R M) : f.coeff.sum single = f

@[deprecated MonoidAlgebra.sum_coeff_single (since := "2026-06-18")]

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

Alias of MonoidAlgebra.sum_coeff_single.

@[deprecated AddMonoidAlgebra.sum_coeff_single (since := "2026-06-18")]

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

Alias of AddMonoidAlgebra.sum_coeff_single.

@[deprecated Finsupp.single_apply (since := "2026-06-18")]

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

@[deprecated Finsupp.single_apply (since := "2026-06-18")]

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

@[deprecated MonoidAlgebra.coeff_single_apply (since := "2026-06-18")]

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).coeff a' = if a = a' then b else 0

Alias of MonoidAlgebra.coeff_single_apply.

@[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 {R : Type u_1} {M : Type u_4} [Semiring R] {motive : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (zero : motive 0) (single_add : ∀ (m : M) (r : R) (x : MonoidAlgebra R M), m ∉ x.coeff.support → r ≠ 0 → motive x → motive (single m r + x)) : motive x

theorem AddMonoidAlgebra.induction {R : Type u_1} {M : Type u_4} [Semiring R] {motive : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M) (zero : motive 0) (single_add : ∀ (m : M) (r : R) (x : AddMonoidAlgebra R M), m ∉ x.coeff.support → r ≠ 0 → motive x → motive (single m r + x)) : motive x

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

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

@[simp]

theorem MonoidAlgebra.addSubmonoidClosure_single {R : Type u_1} {M : Type u_4} [Semiring R] : AddSubmonoid.closure {x : MonoidAlgebra R M | ∃ (m : M) (r : R), x = single m r} = ⊤

@[simp]

theorem AddMonoidAlgebra.addSubmonoidClosure_single {R : Type u_1} {M : Type u_4} [Semiring R] : AddSubmonoid.closure {x : AddMonoidAlgebra R M | ∃ (m : M) (r : R), x = single m r} = ⊤

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

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

@[simp]

theorem MonoidAlgebra.coeff_one_one {R : Type u_1} {M : Type u_4} [Semiring R] [One M] : (coeff 1) 1 = 1

@[simp]

theorem AddMonoidAlgebra.coeff_one_zero {R : Type u_1} {M : Type u_4} [Semiring R] [Zero M] : (coeff 1) 0 = 1

@[deprecated AddMonoidAlgebra.coeff_one_zero (since := "2026-07-15")]

theorem AddMonoidAlgebra.coeff_zero_zero {R : Type u_1} {M : Type u_4} [Semiring R] [Zero M] : (coeff 1) 0 = 1

Alias of AddMonoidAlgebra.coeff_one_zero.

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

The multiplication in an additive monoid algebra.

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

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.

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

@[instance_reducible]

noncomputable instance AddMonoidAlgebra.instMul {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] : Mul (AddMonoidAlgebra 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.

theorem MonoidAlgebra.mul_def {R : Type u_1} {M : Type u_4} [Semiring R] [Mul M] (x y : MonoidAlgebra R M) : x * y = x.coeff.sum fun (m₁ : M) (r₁ : R) => y.coeff.sum 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 = x.coeff.sum fun (m₁ : M) (r₁ : R) => y.coeff.sum fun (m₂ : M) (r₂ : R) => single (m₁ + m₂) (r₁ * r₂)

@[instance_reducible]

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

@[instance_reducible]

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

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

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

@[deprecated MonoidAlgebra.coeff_mul (since := "2026-06-18")]

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).coeff m = x.coeff.sum fun (m₁ : M) (r₁ : R) => y.coeff.sum fun (m₂ : M) (r₂ : R) => if m₁ * m₂ = m then r₁ * r₂ else 0

Alias of MonoidAlgebra.coeff_mul.

@[deprecated AddMonoidAlgebra.coeff_mul (since := "2026-06-18")]

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).coeff m = x.coeff.sum fun (m₁ : M) (r₁ : R) => y.coeff.sum fun (m₂ : M) (r₂ : R) => if m₁ + m₂ = m then r₁ * r₂ else 0

Alias of AddMonoidAlgebra.coeff_mul.

theorem MonoidAlgebra.coeff_mul_antidiag {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).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

theorem AddMonoidAlgebra.coeff_mul_antidiag {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).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

@[deprecated MonoidAlgebra.coeff_mul_antidiag (since := "2026-06-18")]

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).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

Alias of MonoidAlgebra.coeff_mul_antidiag.

@[deprecated AddMonoidAlgebra.coeff_mul_antidiag (since := "2026-06-18")]

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).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

Alias of AddMonoidAlgebra.coeff_mul_antidiag.

@[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.coeff_mul_single_eq_coeff_mul {R : Type u_1} {M : Type u_4} [Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ : M} [Mul M] (m₂ : M) (H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂) : (x * single m r).coeff m₁ = x.coeff m₂ * r

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

@[deprecated MonoidAlgebra.coeff_mul_single_eq_coeff_mul (since := "2026-06-18")]

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} [Mul M] (m₂ : M) (H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂) : (x * single m r).coeff m₁ = x.coeff m₂ * r

Alias of MonoidAlgebra.coeff_mul_single_eq_coeff_mul.

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

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

@[deprecated MonoidAlgebra.coeff_single_mul_eq_mul_coeff (since := "2026-06-18")]

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} [Mul M] (m₂ : M) (H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂) : (single m r * x).coeff m₁ = r * x.coeff m₂

Alias of MonoidAlgebra.coeff_single_mul_eq_mul_coeff.

@[simp]

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

@[simp]

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

@[simp]

theorem MonoidAlgebra.coeff_single_mul_of_forall_mul_ne {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') : (single m r * x).coeff m' = 0

@[simp]

theorem AddMonoidAlgebra.coeff_single_mul_of_forall_add_ne {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') : (single m r * x).coeff m' = 0

@[deprecated MonoidAlgebra.coeff_mul_single_of_forall_mul_ne (since := "2026-06-18")]

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

@[deprecated AddMonoidAlgebra.coeff_mul_single_of_forall_add_ne (since := "2026-06-18")]

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

@[deprecated MonoidAlgebra.coeff_single_mul_of_forall_mul_ne (since := "2026-06-18")]

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

@[deprecated AddMonoidAlgebra.coeff_single_mul_of_forall_add_ne (since := "2026-06-18")]

theorem AddMonoidAlgebra.single_add_apply_of_not_exists_add {R : Type u_1} {M : Type u_4} [Semiring R] [Add M] (r : R) {g g' : M} (x : AddMonoidAlgebra R M) (h : ¬∃ (d : M), g' = g + d) : (single g r * x).coeff g' = 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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_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.ofNat_def {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n = single 1 (OfNat.ofNat n)

theorem AddMonoidAlgebra.ofNat_def {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n = single 0 (OfNat.ofNat n)

@[simp]

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

@[simp]

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

@[simp]

theorem MonoidAlgebra.coeff_ofNat {R : Type u_1} {M : Type u_4} [Semiring R] [MulOneClass M] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).coeff = Finsupp.single 1 (OfNat.ofNat n)

@[simp]

theorem AddMonoidAlgebra.coeff_ofNat {R : Type u_1} {M : Type u_4} [Semiring R] [AddZeroClass M] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).coeff = Finsupp.single 0 (OfNat.ofNat n)

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

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

@[deprecated MonoidAlgebra.coeff_mul_single_one (since := "2026-06-18")]

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).coeff m = x.coeff m * r

Alias of MonoidAlgebra.coeff_mul_single_one.

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

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

@[deprecated MonoidAlgebra.coeff_single_one_mul (since := "2026-06-18")]

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).coeff m = r * x.coeff m

Alias of MonoidAlgebra.coeff_single_one_mul.

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] (a✝ : M) : (of R M) a✝ = single a✝ 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)

@[instance_reducible]

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

@[instance_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] {motive : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (of : ∀ (m : M), motive ((of R M) m)) (add : ∀ (x y : MonoidAlgebra R M), motive x → motive y → motive (x + y)) (smul : ∀ (r : R) (x : MonoidAlgebra R M), motive x → motive (r • x)) : motive 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] [Subsingleton 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] [Subsingleton 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] [Subsingleton M] (a✝ : AddMonoidAlgebra R M) : (uniqueRingEquiv M) a✝ = a✝.coeff 0

@[simp]

theorem MonoidAlgebra.uniqueRingEquiv_apply {R : Type u_1} (M : Type u_4) [Semiring R] [Monoid M] [Subsingleton M] (a✝ : MonoidAlgebra R M) : (uniqueRingEquiv M) a✝ = a✝.coeff 1

@[simp]

theorem MonoidAlgebra.uniqueRingEquiv_symm_apply {R : Type u_1} (M : Type u_4) [Semiring R] [Monoid M] [Subsingleton M] (r : R) : (uniqueRingEquiv M).symm r = single 1 r

@[simp]

theorem AddMonoidAlgebra.uniqueRingEquiv_symm_apply {R : Type u_1} (M : Type u_4) [Semiring R] [AddMonoid M] [Subsingleton M] (r : R) : (uniqueRingEquiv M).symm r = single 0 r

@[simp]

theorem MonoidAlgebra.coeff_uniqueRingEquiv_symm {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] [Subsingleton M] (r : R) (m : M) : ((uniqueRingEquiv M).symm r).coeff m = r

@[simp]

theorem AddMonoidAlgebra.coeff_uniqueRingEquiv_symm {R : Type u_1} {M : Type u_4} [Semiring R] [AddMonoid M] [Subsingleton M] (r : R) (m : M) : ((uniqueRingEquiv M).symm r).coeff m = r

@[deprecated MonoidAlgebra.coeff_uniqueRingEquiv_symm (since := "2026-06-18")]

theorem MonoidAlgebra.uniqueRingEquiv_symm_apply_apply {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] [Subsingleton M] (r : R) (m : M) : ((uniqueRingEquiv M).symm r).coeff m = r

Alias of MonoidAlgebra.coeff_uniqueRingEquiv_symm.

noncomputable def MonoidAlgebra.curryAddEquiv {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.curryAddEquiv {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.curryAddEquiv_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) : curryAddEquiv (single (m, n) r) = single m (single n r)

@[simp]

theorem AddMonoidAlgebra.curryAddEquiv_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) : curryAddEquiv (single (m, n) r) = single m (single n r)

@[simp]

theorem MonoidAlgebra.curryAddEquiv_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) : curryAddEquiv.symm (single m (single n r)) = single (m, n) r

@[simp]

theorem AddMonoidAlgebra.curryAddEquiv_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) : curryAddEquiv.symm (single m (single n r)) = single (m, n) r

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.coeff_mul_single_mul {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] [IsCancelMul M] (x : MonoidAlgebra R M) (r : R) (m m' : M) : (x * single m r).coeff (m' * m) = x.coeff m' * r

@[simp]

theorem AddMonoidAlgebra.coeff_mul_single_add {R : Type u_1} {M : Type u_4} [Semiring R] [AddMonoid M] [IsCancelAdd M] (x : AddMonoidAlgebra R M) (r : R) (m m' : M) : (x * single m r).coeff (m' + m) = x.coeff m' * r

@[simp]

theorem MonoidAlgebra.coeff_single_mul_mul {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] [IsCancelMul M] (x : MonoidAlgebra R M) (r : R) (m m' : M) : (single m r * x).coeff (m * m') = r * x.coeff m'

@[simp]

theorem AddMonoidAlgebra.coeff_single_mul_add {R : Type u_1} {M : Type u_4} [Semiring R] [AddMonoid M] [IsCancelAdd M] (x : AddMonoidAlgebra R M) (r : R) (m m' : M) : (single m r * x).coeff (m + m') = r * x.coeff m'

@[simp]

theorem MonoidAlgebra.coeff_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).coeff h = x.coeff (h * g⁻¹) * r

@[simp]

theorem AddMonoidAlgebra.coeff_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).coeff h = x.coeff (h + -g) * r

@[deprecated MonoidAlgebra.coeff_mul_single_apply (since := "2026-06-18")]

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).coeff h = x.coeff (h * g⁻¹) * r

Alias of MonoidAlgebra.coeff_mul_single_apply.

@[simp]

theorem MonoidAlgebra.coeff_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).coeff h = r * x.coeff (g⁻¹ * h)

@[simp]

theorem AddMonoidAlgebra.coeff_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).coeff h = r * x.coeff (-g + h)

@[deprecated MonoidAlgebra.coeff_single_mul_apply (since := "2026-06-18")]

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).coeff h = r * x.coeff (g⁻¹ * h)

Alias of MonoidAlgebra.coeff_single_mul_apply.

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

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

@[deprecated MonoidAlgebra.coeff_mul_apply_left (since := "2026-06-18")]

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).coeff g = x.coeff.sum fun (h : G) (r : R) => r * y.coeff (h⁻¹ * g)

Alias of MonoidAlgebra.coeff_mul_apply_left.

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

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

@[deprecated MonoidAlgebra.coeff_mul_apply_right (since := "2026-06-18")]

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).coeff g = y.coeff.sum fun (h : G) (r : R) => x.coeff (g * h⁻¹) * r

Alias of MonoidAlgebra.coeff_mul_apply_right.

@[instance_reducible]

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

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

@[instance_reducible]

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

@[instance_reducible]

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

@[simp]

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)

@[simp]

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)

@[simp]

theorem MonoidAlgebra.finsuppProd_single {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [CommSemiring R] [CommMonoid M] [AddCommMonoid N] (f : ι →₀ N) (m : ι → N → M) (r : ι → N → R) : (f.prod fun (i : ι) (n : N) => single (m i n) (r i n)) = single (f.prod m) (f.prod r)

@[simp]

theorem AddMonoidAlgebra.finsuppProd_single {R : Type u_1} {M : Type u_4} {N : Type u_5} {ι : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] (f : ι →₀ N) (m : ι → N → M) (r : ι → N → R) : (f.prod fun (i : ι) (n : N) => single (m i n) (r i n)) = single (f.sum m) (f.prod r)

@[instance_reducible]

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

@[instance_reducible]

noncomputable instance AddMonoidAlgebra.addCommGroup {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.single_neg {R : Type u_1} {M : Type u_4} [Ring R] (m : M) (r : R) : single m (-r) = -single m r

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

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

@[instance_reducible]

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

@[instance_reducible]

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

@[deprecated MonoidAlgebra.coeff_neg (since := "2026-06-18")]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_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] {motive : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M) (of : ∀ (m : M), motive ((of R M) (Multiplicative.ofAdd m))) (add : ∀ (x y : AddMonoidAlgebra R M), motive x → motive y → motive (x + y)) (smul : ∀ (r : R) (x : AddMonoidAlgebra R M), motive x → motive (r • x)) : motive 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)