case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
b : R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum (b • { toFinsupp := toFinsupp✝ }) f = sum { toFinsupp := toFinsupp✝ } fun n a => f n (b * a)
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]
b : R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
⊢ sum (b • p) f = sum p fun n a => f n (b * a)
rcases p with ⟨⟩
no goals
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
b : R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ sum (b • { toFinsupp := toFinsupp✝ }) f = sum { toFinsupp := toFinsupp✝ } fun n a => f n (b * a)
simpa [sum, support, coeff] using Finsupp.sum_smul_index hf