R : Type u
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : support p ⊆ s
n : ℕ
_hn : n ∈ s
h'n : ¬n ∈ support p
⊢ f n (coeff p n) = 0
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : support p ⊆ s
⊢ sum p f = ∑ n in s, f n (coeff p n)
refine Finset.sum_subset hs fun n _hn h'n => ?_
R : Type u
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : support p ⊆ s
n : ℕ
_hn : n ∈ s
h'n : coeff p n = 0
⊢ f n (coeff p n) = 0
R : Type u
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : support p ⊆ s
n : ℕ
_hn : n ∈ s
h'n : ¬n ∈ support p
⊢ f n (coeff p n) = 0
rw [not_mem_support_iff] at h'n
no goals
R : Type u
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : support p ⊆ s
n : ℕ
_hn : n ∈ s
h'n : coeff p n = 0
⊢ f n (coeff p n) = 0
simp [h'n, hf]