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 : MvPolynomial σ R
P : MvPolynomial σ R → Prop
p : MvPolynomial σ R
h1 : ∀ (u : σ →₀ ℕ) (a : R), P (↑(monomial u) a)
h2 : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)
this : P (↑(monomial 0) 0)
⊢ P 0
rwa [monomial_zero] at this