Monoid algebras

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

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

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

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

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

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

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

Notation

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

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

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

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

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

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

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

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

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

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

def AddMonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for AddMonoidAlgebra.

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

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

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

def MonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for MonoidAlgebra.

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

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

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

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

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

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

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

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

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

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

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

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

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

A copy of Finsupp.ext for MonoidAlgebra.

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

A copy of Finsupp.ext for AddMonoidAlgebra.

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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 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 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.smul_apply {R : Type u_1} {M : Type u_4} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : MonoidAlgebra R M) (m : M) : (a • x) m = a • x m

@[simp]

theorem AddMonoidAlgebra.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) (m : M) : (a • x) m = a • x m

@[simp]

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

@[simp]

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

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

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

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 AddMonoidAlgebra.distribSMul {R : Type u_1} {M : Type u_4} {N : Type u_5} [Semiring R] [DistribSMul N R] : DistribSMul N (AddMonoidAlgebra R M)

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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.

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

AddMonoidAlgebra.single as an AddMonoidHom.

TODO: Rename to singleAddMonoidHom.

@[simp]

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

@[simp]

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

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

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

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

TODO: Rename to addMonoidHom_ext'.

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

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

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

TODO: Rename to addMonoidHom_ext'.

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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 AddMonoidAlgebra.zero {R : Type u_1} {M : Type u_4} [Semiring R] [Zero M] : One (AddMonoidAlgebra R M)

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

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

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

@[irreducible]

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

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

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

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

(Think of the group ring of a group.)

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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 MonoidAlgebra.nonUnitalSemiring {R : Type u_1} {M : Type u_4} [Semiring R] [Semigroup M] : NonUnitalSemiring (MonoidAlgebra R M)

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

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

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

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

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

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

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

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

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

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

The embedding of a unital magma into its magma algebra.

@[simp]

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

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

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

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

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

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 MonoidAlgebra.semiring {R : Type u_1} {M : Type u_4} [Semiring R] [Monoid M] : Semiring (MonoidAlgebra R M)

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

@[simp]

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

@[simp]

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

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

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

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

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

The trivial monoid algebra is the base ring.

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

The trivial additive monoid algebra is the base ring.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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 MonoidAlgebra.commSemiring {R : Type u_1} {M : Type u_4} [CommSemiring R] [CommMonoid M] : CommSemiring (MonoidAlgebra R M)

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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 MonoidAlgebra.ring {R : Type u_1} {M : Type u_4} [Ring R] [Monoid M] : Ring (MonoidAlgebra R M)

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

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

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

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

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

Additive monoids

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

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.

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

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

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

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

@[simp]

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

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

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

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

See note [partially-applied ext lemmas].

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