no goals
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → Monic (f i)
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
simpa using natDegree_multiset_prod_of_monic (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 : ι), i ∈ s → Monic (f i)
⊢ ∀ (f_1 : R[X]), f_1 ∈ Multiset.map f s.val → Monic f_1
simpa using h