σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ support x
⊢ (∃ si, si ∈ s ∧ si ≤ xi) ↔ ∃ si, si ∈ s ∧ ↑(monomial si) 1 ∣ ↑(monomial xi) (coeff xi x)
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s => ↑(monomial s) 1) '' s) ↔
    ∀ (xi : σ →₀ ℕ), xi ∈ support x → ∃ si, si ∈ s ∧ ↑(monomial si) 1 ∣ ↑(monomial xi) (coeff xi x)
refine' mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => _)
no goals
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ support x
⊢ (∃ si, si ∈ s ∧ si ≤ xi) ↔ ∃ si, si ∈ s ∧ ↑(monomial si) 1 ∣ ↑(monomial xi) (coeff xi x)
simp_rw [monomial_dvd_monomial, one_dvd, and_true_iff, mem_support_iff.mp hxi, false_or_iff]