English
For φ ∈ MvPolynomial σ R and i ∈ ℕ, the ith coordinate of decomposition.decompose' φ equals the ith homogeneous component of φ.
Русский
Для φ и i, i-ая координата decomposition.decompose' φ равна i-ой однородной компоненте φ.
LaTeX
$$(decomposition.decompose' φ) i = homogeneousComponent i φ$$
Lean4
/-- `x` is in a monomial ideal generated by `s` iff every element of its support dominates one of
the generators. Note that `si ≤ xi` is analogous to saying that the monomial corresponding to `si`
divides the monomial corresponding to `xi`. -/
theorem mem_ideal_span_monomial_image {x : MvPolynomial σ R} {s : Set (σ →₀ ℕ)} :
x ∈ Ideal.span ((fun s => monomial s (1 : R)) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi :=
by
refine AddMonoidAlgebra.mem_ideal_span_of'_image.trans ?_
simp_rw [le_iff_exists_add, add_comm]
rfl
