English
The monomial ideals generated by X_i form a foundational example: x is in span(X '' s) iff every monomial in x’s support has a nonzero X-component.
Русский
Мономиальные идеалы, порожденные X_i, задают базовый пример: x в span(X'' s) тогда, когда каждая мономиальная компонента в поддержке x имеет ненулевой разложение по X.
LaTeX
$$x ∈ span (X '' s) ⇔ ∀ m ∈ x.support, ∃ i ∈ s, (m i) ≠ 0$$
Lean4
/-- `x` is in a monomial ideal generated by variables `X` iff every element of its support
has a component in `s`. -/
theorem mem_ideal_span_X_image {x : MvPolynomial σ R} {s : Set σ} :
x ∈ Ideal.span (MvPolynomial.X '' s : Set (MvPolynomial σ R)) ↔ ∀ m ∈ x.support, ∃ i ∈ s, (m : σ →₀ ℕ) i ≠ 0 :=
by
have := @mem_ideal_span_monomial_image σ R _ x ((fun i => Finsupp.single i 1) '' s)
rw [Set.image_image] at this
refine this.trans ?_
simp [Nat.one_le_iff_ne_zero]
