MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul
theorem MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul :
∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : Mul A] {f g : MonoidAlgebra R A} {a0 b0 : A},
UniqueMul f.support g.support a0 b0 → (f * g) (a0 * b0) = f a0 * g b0
This theorem states that for any semiring `R`, any type `A` with a multiplication operation, and any two monoid algebras `f` and `g` over `R` and `A`, if the product of two elements `a0` and `b0` from the support sets of `f` and `g` respectively can be written in at most one way as a product of elements from these support sets, then the coefficient of the monomial identified by the product `a0 * b0` in the product `f * g` of the two monoid algebras is equal to the product of the coefficients of the monomials identified by `a0` and `b0` in `f` and `g` respectively. In other words, this theorem states that under the given uniqueness condition, the convolution product in the monoid algebra behaves like usual multiplication for the involved elements.
More concisely: Given two monoid algebras `f` and `g` over a semiring `R` and type `A` with unique product representations in their support sets, the convolution product of `f` and `g` agrees with the usual multiplication of their coefficients on matched monomials.
|
AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd
theorem AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd :
∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : Add A] {f g : AddMonoidAlgebra R A} {a0 b0 : A},
UniqueAdd f.support g.support a0 b0 → (f * g) (a0 + b0) = f a0 * g b0
This theorem states that in the context of an additive monoid algebra over a semiring `R`, given two elements `f` and `g` of this algebra, and two elements `a0` and `b0` from the additive monoid, if `a0 + b0` can be expressed in a unique way as the sum of an element from the support of `f` and an element from the support of `g`, then the coefficient of the monomial `a0 + b0` in the product `f * g` is equal to the product of the coefficients of `a0` and `b0` in `f` and `g` respectively. In other words, the product rule applies to find the coefficient of a monomial in the polynomial product `f * g`, when the monomial can be uniquely expressed as a sum of monomials from `f` and `g`.
More concisely: Given additive monoids `M` and an additive monoid algebra `A` over a semiring `R`, if `f, g ∈ A` and there exists unique `x ∈ M` such that `x = a0 + a1` with `a0 ∈ supp(f)` and `a1 ∈ supp(g)`, then the coefficient of `x` in `f * g` is equal to the product of the coefficients of `a0` in `f` and `a1` in `g`.
|