no goals
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∏ i in s, leadingCoeff (f i) ≠ 0
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
simpa using natDegree_multiset_prod' (s.1.map f) (by simpa using h)
no goals
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∏ i in s, leadingCoeff (f i) ≠ 0
⊢ prod (Multiset.map (fun f => leadingCoeff f) (Multiset.map f s.val)) ≠ 0
simpa using h