case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
q r : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (sum { toFinsupp := toFinsupp✝ } f) n = sum { toFinsupp := toFinsupp✝ } fun a b => coeff (f a b) n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
⊢ coeff (sum p f) n = sum p fun a b => coeff (f a b) n
rcases p with ⟨⟩
no goals
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
q r : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (sum { toFinsupp := toFinsupp✝ } f) n = sum { toFinsupp := toFinsupp✝ } fun a b => coeff (f a b) n
simp [Polynomial.sum, support_ofFinsupp, coeff_ofFinsupp]