case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ (p : R[X]), p ∈ Quotient.mk (List.isSetoid R[X]) a✝ → natDegree p ≤ n
⊢ coeff (prod (Quotient.mk (List.isSetoid R[X]) a✝)) (↑Multiset.card (Quotient.mk (List.isSetoid R[X]) a✝) * n) =
    prod (Multiset.map (fun p => coeff p n) (Quotient.mk (List.isSetoid R[X]) a✝))
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
n : ℕ
hl : ∀ (p : R[X]), p ∈ t → natDegree p ≤ n
⊢ coeff (prod t) (↑Multiset.card t * n) = prod (Multiset.map (fun p => coeff p n) t)
induction t using Quotient.inductionOn
no goals
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ (p : R[X]), p ∈ Quotient.mk (List.isSetoid R[X]) a✝ → natDegree p ≤ n
⊢ coeff (prod (Quotient.mk (List.isSetoid R[X]) a✝)) (↑Multiset.card (Quotient.mk (List.isSetoid R[X]) a✝) * n) =
    prod (Multiset.map (fun p => coeff p n) (Quotient.mk (List.isSetoid R[X]) a✝))
simpa using coeff_list_prod_of_natDegree_le _ _ hl