Total Monoid Algebras

This file mirrors the construction in MonoidAlgebra/Defs.lean, but drops the finiteness condition on the support of the elements. In the literature, this construction is called the "large algebra of a monoid" or "total algebra" (see https://en.wikipedia.org/wiki/Total_algebra). When the underlying monoid is finitely supported functions valued in ℕ, this construction corresponds to the multivariate formal power series in the large sense, where arbitrary infinite sums of monomials are permitted.

structure TotalAddMonoidAlgebra (R : Type u_1) (M : Type u_2) [Semiring R] : Type (max u_1 u_2)

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

It is the type of all 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 total additive monoid algebra R⟦M⟧.

• )

structure TotalMonoidAlgebra (R : Type u_1) (M : Type u_2) [Semiring R] : Type (max u_1 u_2)

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

It is the type of all 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 total monoid algebra R⟦M⟧.

• )

def TotalAddMonoidAlgebra.«term__⟦_⟧» : Lean.TrailingParserDescr

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

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

Equations

• One or more equations did not get rendered due to their size.

def TotalAddMonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for TotalAddMonoidAlgebra.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• TotalAddMonoidAlgebra.delabOfCoeff = Lean.PrettyPrinter.Delaborator.delabApp

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

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

Equations

• TotalMonoidAlgebra.delabOfCoeff = Lean.PrettyPrinter.Delaborator.delabApp

def TotalMonoidAlgebra.«term__⟦_⟧» : Lean.TrailingParserDescr

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

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

Equations

• One or more equations did not get rendered due to their size.

def TotalMonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for TotalMonoidAlgebra.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

def TotalMonoidAlgebra.coeffEquiv {R : Type u_1} {M : Type u_2} [Semiring R] : TotalMonoidAlgebra R M ≃ (M → R)

TotalMonoidAlgebra.coeff as an equiv.

Equations

• TotalMonoidAlgebra.coeffEquiv = { toFun := TotalMonoidAlgebra.coeff, invFun := TotalMonoidAlgebra.ofCoeff, left_inv := ⋯, right_inv := ⋯ }

def TotalAddMonoidAlgebra.coeffEquiv {R : Type u_1} {M : Type u_2} [Semiring R] : TotalAddMonoidAlgebra R M ≃ (M → R)

TotalAddMonoidAlgebra.coeff as an equiv.

Equations

• TotalAddMonoidAlgebra.coeffEquiv = { toFun := TotalAddMonoidAlgebra.coeff, invFun := TotalAddMonoidAlgebra.ofCoeff, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem TotalMonoidAlgebra.coeffEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] {x : TotalMonoidAlgebra R M} : coeffEquiv x = x.coeff

@[simp]

theorem TotalAddMonoidAlgebra.coeffEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] {x : TotalAddMonoidAlgebra R M} : coeffEquiv x = x.coeff

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

theorem TotalMonoidAlgebra.ofCoeff_inj {R : Type u_1} {M : Type u_2} [Semiring R] {x y : M → R} : ofCoeff x = ofCoeff y ↔ x = y

theorem TotalAddMonoidAlgebra.ofCoeff_inj {R : Type u_1} {M : Type u_2} [Semiring R] {x y : M → R} : ofCoeff x = ofCoeff y ↔ x = y

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

Alias of the forward direction of TotalMonoidAlgebra.coeff_inj.

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

Alias of the forward direction of TotalAddMonoidAlgebra.coeff_inj.

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

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

@[instance_reducible]

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

Equations

• TotalMonoidAlgebra.instInhabited = { default := TotalMonoidAlgebra.ofCoeff 0 }

@[instance_reducible]

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

Equations

• TotalAddMonoidAlgebra.instInhabited = { default := TotalAddMonoidAlgebra.ofCoeff 0 }

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

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

@[instance_reducible]

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

Equations

• TotalMonoidAlgebra.instUnique = { default := TotalMonoidAlgebra.ofCoeff 0, uniq := ⋯ }

@[instance_reducible]

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

Equations

• TotalAddMonoidAlgebra.instUnique = { default := TotalAddMonoidAlgebra.ofCoeff 0, uniq := ⋯ }

@[instance_reducible]

instance TotalMonoidAlgebra.instAddMonoid {R : Type u_1} {M : Type u_2} [Semiring R] : AddMonoid (TotalMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TotalAddMonoidAlgebra.instAddMonoid {R : Type u_1} {M : Type u_2} [Semiring R] : AddMonoid (TotalAddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TotalMonoidAlgebra.instAddCommMonoid {R : Type u_1} {M : Type u_2} [Semiring R] : AddCommMonoid (TotalMonoidAlgebra R M)

Equations

• TotalMonoidAlgebra.instAddCommMonoid = { toAddMonoid := TotalMonoidAlgebra.instAddMonoid, add_comm := ⋯ }

@[instance_reducible]

instance TotalAddMonoidAlgebra.instAddCommMonoid {R : Type u_1} {M : Type u_2} [Semiring R] : AddCommMonoid (TotalAddMonoidAlgebra R M)

Equations

• TotalAddMonoidAlgebra.instAddCommMonoid = { toAddMonoid := TotalAddMonoidAlgebra.instAddMonoid, add_comm := ⋯ }

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

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

def TotalMonoidAlgebra.coeffAddEquiv {R : Type u_1} {M : Type u_2} [Semiring R] : TotalMonoidAlgebra R M ≃+ (M → R)

TotalMonoidAlgebra.coeff as an AddEquiv.

Equations

• TotalMonoidAlgebra.coeffAddEquiv = TotalMonoidAlgebra.coeffEquiv.addEquiv

def TotalAddMonoidAlgebra.coeffAddEquiv {R : Type u_1} {M : Type u_2} [Semiring R] : TotalAddMonoidAlgebra R M ≃+ (M → R)

TotalAddMonoidAlgebra.coeff as an AddEquiv.

Equations

• TotalAddMonoidAlgebra.coeffAddEquiv = TotalAddMonoidAlgebra.coeffEquiv.addEquiv

@[simp]

theorem TotalAddMonoidAlgebra.coeffAddEquiv_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] (coeff : M → R) : coeffAddEquiv.symm coeff = ofCoeff coeff

@[simp]

theorem TotalMonoidAlgebra.coeffAddEquiv_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] (coeff : M → R) : coeffAddEquiv.symm coeff = ofCoeff coeff

@[simp]

theorem TotalAddMonoidAlgebra.coeffAddEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] (self : TotalAddMonoidAlgebra R M) (a✝ : M) : coeffAddEquiv self a✝ = self.coeff a✝

@[simp]

theorem TotalMonoidAlgebra.coeffAddEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] (self : TotalMonoidAlgebra R M) (a✝ : M) : coeffAddEquiv self a✝ = self.coeff a✝

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem TotalMonoidAlgebra.ofCoeff_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] {x : M → R} : ofCoeff x = 0 ↔ x = 0

@[simp]

theorem TotalAddMonoidAlgebra.ofCoeff_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] {x : M → R} : ofCoeff x = 0 ↔ x = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem TotalMonoidAlgebra.ofCoeff_sum {R : Type u_1} {M : Type u_2} {ι : Type u_5} [Semiring R] (s : Finset ι) (f : ι → M → R) : ofCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, ofCoeff (f i)

@[simp]

theorem TotalAddMonoidAlgebra.ofCoeff_sum {R : Type u_1} {M : Type u_2} {ι : Type u_5} [Semiring R] (s : Finset ι) (f : ι → M → R) : ofCoeff (∑ i ∈ s, f i) = ∑ i ∈ s, ofCoeff (f i)

@[simp]

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

@[simp]

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

@[simp]

theorem TotalMonoidAlgebra.ofCoeff_finsuppSum {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_5} [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 TotalAddMonoidAlgebra.ofCoeff_finsuppSum {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_5} [Semiring R] [AddCommMonoid N] (f : ι →₀ N) (g : ι → N → M → R) : ofCoeff (f.sum g) = f.sum fun (i : ι) (n : N) => ofCoeff (g i n)

def TotalMonoidAlgebra.single {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) : TotalMonoidAlgebra R M

TotalMonoidAlgebra.single m r for m : M, r : R is the element rm : R⟦M⟧.

Equations

• TotalMonoidAlgebra.single m r = TotalMonoidAlgebra.ofCoeff (Pi.single m r)

def TotalAddMonoidAlgebra.single {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) : TotalAddMonoidAlgebra R M

TotalAddMonoidAlgebra.single m r for m : M, r : R is the element rm : R⟦M⟧.

Equations

• TotalAddMonoidAlgebra.single m r = TotalAddMonoidAlgebra.ofCoeff (Pi.single m r)

@[simp]

theorem TotalMonoidAlgebra.coeff_single {R : Type u_1} {M : Type u_2} [Semiring R] (m : M) (r : R) [DecidableEq M] : (single m r).coeff = Pi.single m r

@[simp]

theorem TotalAddMonoidAlgebra.coeff_single {R : Type u_1} {M : Type u_2} [Semiring R] (m : M) (r : R) [DecidableEq M] : (single m r).coeff = Pi.single m r

@[simp]

theorem TotalMonoidAlgebra.ofCoeff_single {R : Type u_1} {M : Type u_2} [Semiring R] (m : M) (r : R) [DecidableEq M] : ofCoeff (Pi.single m r) = single m r

@[simp]

theorem TotalAddMonoidAlgebra.ofCoeff_single {R : Type u_1} {M : Type u_2} [Semiring R] (m : M) (r : R) [DecidableEq M] : ofCoeff (Pi.single m r) = single m r

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

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

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

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

@[simp]

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

@[simp]

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

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

TotalMonoidAlgebra.single m r is injective in m if r ≠ 0. For injectivity in r, see TotalMonoidAlgebra.single_right_injective.

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

TotalAddMonoidAlgebra.single m r is injective in m if r ≠ 0. For injectivity in r, see TotalAddMonoidAlgebra.single_right_injective.

theorem TotalMonoidAlgebra.single_right_injective {R : Type u_1} {M : Type u_2} [Semiring R] {m : M} [DecidableEq M] : Function.Injective (single m)

theorem TotalAddMonoidAlgebra.single_right_injective {R : Type u_1} {M : Type u_2} [Semiring R] {m : M} [DecidableEq M] : Function.Injective (single m)

def TotalMonoidAlgebra.update {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) (x : TotalMonoidAlgebra R M) : TotalMonoidAlgebra R M

Replace the m-th coefficient of an element x of the total monoid algebra by a given value r : R.

Equations

• TotalMonoidAlgebra.update m r x = TotalMonoidAlgebra.ofCoeff (Function.update x.coeff m r)

def TotalAddMonoidAlgebra.update {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) (x : TotalAddMonoidAlgebra R M) : TotalAddMonoidAlgebra R M

Replace the m-th coefficient of an element x of the total additive monoid algebra by a given value r : R.

Equations

• TotalAddMonoidAlgebra.update m r x = TotalAddMonoidAlgebra.ofCoeff (Function.update x.coeff m r)

@[simp]

theorem TotalMonoidAlgebra.coeff_update {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) (x : TotalMonoidAlgebra R M) : (update m r x).coeff = Function.update x.coeff m r

@[simp]

theorem TotalAddMonoidAlgebra.coeff_update {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) (x : TotalAddMonoidAlgebra R M) : (update m r x).coeff = Function.update x.coeff m r

@[simp]

theorem TotalMonoidAlgebra.ofCoeff_update {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) (x : M → R) : ofCoeff (Function.update x m r) = update m r (ofCoeff x)

@[simp]

theorem TotalAddMonoidAlgebra.ofCoeff_update {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) (x : M → R) : ofCoeff (Function.update x m r) = update m r (ofCoeff x)

@[instance_reducible]

instance TotalMonoidAlgebra.smulZeroClass {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] : SMulZeroClass A (TotalMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TotalAddMonoidAlgebra.smulZeroClass {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] : SMulZeroClass A (TotalAddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TotalMonoidAlgebra.coeff_smul {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] (a : A) (x : TotalMonoidAlgebra R M) : (a • x).coeff = a • x.coeff

@[simp]

theorem TotalAddMonoidAlgebra.coeff_smul {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] (a : A) (x : TotalAddMonoidAlgebra R M) : (a • x).coeff = a • x.coeff

@[simp]

theorem TotalMonoidAlgebra.ofCoeff_smul {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] (a : A) (x : M → R) : ofCoeff (a • x) = a • ofCoeff x

@[simp]

theorem TotalAddMonoidAlgebra.ofCoeff_smul {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] (a : A) (x : M → R) : ofCoeff (a • x) = a • ofCoeff x

theorem TotalMonoidAlgebra.coeff_smul_apply {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] (a : A) (x : TotalMonoidAlgebra R M) (m : M) : (a • x).coeff m = a • x.coeff m

theorem TotalAddMonoidAlgebra.coeff_smul_apply {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] (a : A) (x : TotalAddMonoidAlgebra R M) (m : M) : (a • x).coeff m = a • x.coeff m

@[simp]

theorem TotalMonoidAlgebra.smul_single {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] [DecidableEq M] (a : A) (m : M) (r : R) : a • single m r = single m (a • r)

@[simp]

theorem TotalAddMonoidAlgebra.smul_single {R : Type u_1} {M : Type u_2} [Semiring R] {A : Type u_6} [SMulZeroClass A R] [DecidableEq M] (a : A) (m : M) (r : R) : a • single m r = single m (a • r)

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

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

@[instance_reducible]

instance TotalMonoidAlgebra.distribSMul {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [DistribSMul N R] : DistribSMul N (TotalMonoidAlgebra R M)

Equations

• TotalMonoidAlgebra.distribSMul = { toSMulZeroClass := TotalMonoidAlgebra.smulZeroClass, smul_add := ⋯ }

@[instance_reducible]

instance TotalAddMonoidAlgebra.distribSMul {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [DistribSMul N R] : DistribSMul N (TotalAddMonoidAlgebra R M)

Equations

• TotalAddMonoidAlgebra.distribSMul = { toSMulZeroClass := TotalAddMonoidAlgebra.smulZeroClass, smul_add := ⋯ }

instance TotalMonoidAlgebra.isScalarTower {R : Type u_1} {M : Type u_2} {N : Type u_3} {O : Type u_4} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] : IsScalarTower N O (TotalMonoidAlgebra R M)

instance TotalAddMonoidAlgebra.isScalarTower {R : Type u_1} {M : Type u_2} {N : Type u_3} {O : Type u_4} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] : IsScalarTower N O (TotalAddMonoidAlgebra R M)

instance TotalMonoidAlgebra.smulCommClass {R : Type u_1} {M : Type u_2} {N : Type u_3} {O : Type u_4} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] : SMulCommClass N O (TotalMonoidAlgebra R M)

instance TotalAddMonoidAlgebra.smulCommClass {R : Type u_1} {M : Type u_2} {N : Type u_3} {O : Type u_4} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] : SMulCommClass N O (TotalAddMonoidAlgebra R M)

instance TotalMonoidAlgebra.isCentralScalar {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] : IsCentralScalar N (TotalMonoidAlgebra R M)

instance TotalAddMonoidAlgebra.isCentralScalar {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] : IsCentralScalar N (TotalAddMonoidAlgebra R M)

@[simp]

theorem TotalMonoidAlgebra.single_zero {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) : single m 0 = 0

@[simp]

theorem TotalAddMonoidAlgebra.single_zero {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) : single m 0 = 0

@[simp]

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

@[simp]

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

def TotalMonoidAlgebra.singleAddMonoidHom {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) : R →+ TotalMonoidAlgebra R M

TotalMonoidAlgebra.single as an AddMonoidHom.

Equations

• TotalMonoidAlgebra.singleAddMonoidHom m = { toFun := TotalMonoidAlgebra.single m, map_zero' := ⋯, map_add' := ⋯ }

def TotalAddMonoidAlgebra.singleAddAddMonoidHom {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) : R →+ TotalAddMonoidAlgebra R M

TotalAddMonoidAlgebra.single as an AddMonoidHom.

Equations

• TotalAddMonoidAlgebra.singleAddAddMonoidHom m = { toFun := TotalAddMonoidAlgebra.single m, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TotalMonoidAlgebra.singleAddMonoidHom_apply {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) : (singleAddMonoidHom m) r = single m r

@[simp]

theorem TotalAddMonoidAlgebra.singleAddAddMonoidHom_apply {R : Type u_1} {M : Type u_2} [Semiring R] [DecidableEq M] (m : M) (r : R) : (singleAddAddMonoidHom m) r = single m r

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

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

@[simp]

theorem TotalMonoidAlgebra.single_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] {r : R} {m : M} [DecidableEq M] : single m r = 0 ↔ r = 0

@[simp]

theorem TotalAddMonoidAlgebra.single_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] {r : R} {m : M} [DecidableEq M] : single m r = 0 ↔ r = 0

theorem TotalMonoidAlgebra.single_ne_zero {R : Type u_1} {M : Type u_2} [Semiring R] {r : R} {m : M} [DecidableEq M] : single m r ≠ 0 ↔ r ≠ 0

theorem TotalAddMonoidAlgebra.single_ne_zero {R : Type u_1} {M : Type u_2} [Semiring R] {r : R} {m : M} [DecidableEq M] : single m r ≠ 0 ↔ r ≠ 0