R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q p : MvPolynomial σ R
⊢ p ≠ 0 ↔ ∃ d, coeff d p ≠ 0
rw [Ne.def, eq_zero_iff]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q p : MvPolynomial σ R
⊢ (∃ d, coeff d p ≠ 0) ↔ ∃ d, coeff d p ≠ 0
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0
push_neg
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q p : MvPolynomial σ R
⊢ (∃ d, coeff d p ≠ 0) ↔ ∃ d, coeff d p ≠ 0
rfl