Lemmas about ideals of MonoidAlgebra and AddMonoidAlgebra

theorem MonoidAlgebra.mem_ideal_span_of_image {k : Type u_1} {G : Type u_3} [Monoid G] [Semiring k] {s : Set G} {x : MonoidAlgebra k G} : x ∈ Ideal.span (⇑(of k G) '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : G), m = d * m'

If x belongs to the ideal generated by generators in s, then every element of the support of x factors through an element of s.

We could spell ∃ d, m = d * m as MulOpposite.op m' ∣ MulOpposite.op m but this would be worse.

theorem AddMonoidAlgebra.mem_ideal_span_of'_image {k : Type u_1} {A : Type u_2} [AddMonoid A] [Semiring k] {s : Set A} {x : AddMonoidAlgebra k A} : x ∈ Ideal.span (of' k A '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ (d : A), m = d + m'

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.