no goals
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
⊢ degree (∏ i in s, f i) ≤ ∑ i in s, degree (f i)
simpa only [Multiset.map_map] using degree_multiset_prod_le (s.1.map f)