R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.373398
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
this : n ∈ {0}
⊢ (sum n fun x e => e) ≤ 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.373398
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
⊢ (sum n fun x e => e) ≤ 0
have := Finsupp.support_single_subset hn
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.373398
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
this : n = 0
⊢ (sum n fun x e => e) ≤ 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.373398
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
this : n ∈ {0}
⊢ (sum n fun x e => e) ≤ 0
rw [Finset.mem_singleton] at this
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.373398
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
hn : 0 ∈ support (↑C a)
⊢ (sum 0 fun x e => e) ≤ 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.373398
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
n : σ →₀ ℕ
hn : n ∈ support (↑C a)
this : n = 0
⊢ (sum n fun x e => e) ≤ 0
subst this
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.373398
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
a : R
hn : 0 ∈ support (↑C a)
⊢ (sum 0 fun x e => e) ≤ 0
exact le_rfl