English
In additive context, the same factorization property holds with addition: x in the span of AddMonoidAlgebra.of' k A '' s iff every element of its support factors additively through s.
Русский
В аддитивном контексте выполняется аналогичное свойство факторизации через элементы s для опоры x.
LaTeX
$$$x \in \mathrm{Ideal}.\mathrm{span}(\mathrm{AddMonoidAlgebra}.of' k A '' s) \iff \forall m \in x.support, \exists m' \in s, \exists d, m = d + m'$$$
Lean4
/-- If `x` belongs to the ideal generated by generators in `s`, then every element of the support of
`x` factors additively through an element of `s`.
-/
theorem mem_ideal_span_of'_image [AddMonoid A] [Semiring k] {s : Set A} {x : AddMonoidAlgebra k A} :
x ∈ Ideal.span (AddMonoidAlgebra.of' k A '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d + m' :=
@MonoidAlgebra.mem_ideal_span_of_image k (Multiplicative A) _ _ _ _
