Lemmas about ideals of monoid_algebra and add_monoid_algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
monoid_algebra.mem_ideal_span_of_image
{k : Type u_1}
{G : Type u_3}
[monoid G]
[semiring k]
{s : set G}
{x : monoid_algebra k G} :
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 mul_opposite.op m' ∣ mul_opposite.op m but this would be worse.
theorem
add_monoid_algebra.mem_ideal_span_of'_image
{k : Type u_1}
{A : Type u_2}
[add_monoid A]
[semiring k]
{s : set A}
{x : add_monoid_algebra k A} :
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.