MonoidAlgebra.support_mul
theorem MonoidAlgebra.support_mul :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G]
(a b : MonoidAlgebra k G), (a * b).support ⊆ a.support * b.support
The theorem `MonoidAlgebra.support_mul` states that for any semiring `k` and any type `G` that has both multiplication and decidable equality, if `a` and `b` are elements of the monoid algebra of `G` over `k`, then the support of the product of `a` and `b` is a subset of the product of the supports of `a` and `b`. In mathematical terms, given $\alpha, \beta \in G \rightarrow k$ (elements of the monoid algebra), the support of $\alpha\beta$ is contained within the set product of the supports of $\alpha$ and $\beta$. The support of a function in this context is the set of points where the function is non-zero.
More concisely: For any semiring `k` and type `G` with multiplication and decidable equality, the support of the product of two elements in the monoid algebra of `G` over `k` is contained in the product of their supports.
|
AddMonoidAlgebra.support_mul
theorem AddMonoidAlgebra.support_mul :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : DecidableEq G] [inst_2 : Add G]
(a b : AddMonoidAlgebra k G), (a * b).support ⊆ a.support + b.support
The theorem `AddMonoidAlgebra.support_mul` states that for any given types `k` and `G`, where `k` is a semiring and `G` has decidable equality and an additive structure, if `a` and `b` are elements of the monoid algebra of `G` over `k`, then the support of the product of `a` and `b` (denoted `(a * b).support`) is a subset of the sum of the supports of `a` and `b` (denoted `a.support + b.support`). Here, "support" refers to the set of nonzero elements in a given element of the monoid algebra.
More concisely: For any semiring `k` and additive type `G` with decidable equality, the support of the product of two elements in the monoid algebra of `G` over `k` is a subset of the sum of their supports.
|
AddMonoidAlgebra.mem_span_support'
theorem AddMonoidAlgebra.mem_span_support' :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] (f : AddMonoidAlgebra k G),
f ∈ Submodule.span k (AddMonoidAlgebra.of' k G '' ↑f.support)
This theorem states that for any semiring `k` and any type `G`, any element `f` of the monoid algebra `AddMonoidAlgebra k G` (which is the `k`-linear combinations of terms of `G`) is contained in the submodule generated by its support. Here, the support of `f` is the set of `G` such that `f` is nonzero, and `Submodule.span k` is the smallest submodule of the monoid algebra containing this set. The mapping `AddMonoidAlgebra.of' k G` provides the embedding of `G` into the monoid algebra. In other words, each element of the monoid algebra can be expressed as a `k`-linear combination of elements from its support.
More concisely: For any semiring `k` and type `G`, every element `f` in the monoid algebra `AddMonoidAlgebra k G` is contained in the submodule generated by its support.
|
MonoidAlgebra.mem_span_support
theorem MonoidAlgebra.mem_span_support :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : MulOneClass G] (f : MonoidAlgebra k G),
f ∈ Submodule.span k (⇑(MonoidAlgebra.of k G) '' ↑f.support)
This theorem states that, for any given element 'f' of the monoid algebra (denoted as `MonoidAlgebra k G`) over a semiring 'k' generated by the monoid 'G', the element 'f' is contained within the subalgebra generated by its support. The support of 'f' is the set of all elements of the monoid that have a non-zero coefficient in the formal linear combination that represents 'f'. The subalgebra generated by the support of 'f' is the smallest submodule of the monoid algebra that contains the image of the support under the monoid algebra embedding (`MonoidAlgebra.of k G`), which maps elements of the monoid to the monoid algebra.
More concisely: For any element 'f' in the monoid algebra `MonoidAlgebra k G`, the subalgebra generated by the support of 'f' contains 'f'.
|
AddMonoidAlgebra.mem_span_support
theorem AddMonoidAlgebra.mem_span_support :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : AddZeroClass G] (f : AddMonoidAlgebra k G),
f ∈ Submodule.span k (⇑(AddMonoidAlgebra.of k G) '' ↑f.support)
The theorem `AddMonoidAlgebra.mem_span_support` states that for any semiring `k` and additive monoid `G` with zero, any element `f` of the monoid algebra `k[G]` is contained within the submodule generated by its support. In other words, `f` can be expressed as a linear combination of elements from the image under the embedding of the support set of `f` into the monoid algebra `k[G]`.
More concisely: For any semiring `k` and additive monoid `G` with zero, every element `f` in the monoid algebra `k[G]` lies in the submodule generated by the image of its support under the embedding of `G` into `k[G]`.
|