Documentation

Mathlib.Algebra.MonoidAlgebra.Ideal

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 ((MonoidAlgebra.of k G) '' s) mx.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 (AddMonoidAlgebra.of' k A '' s) mx.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.