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
⊢ leadingCoeff (∏ i in s, f i) = ∏ i in s, leadingCoeff (f i)
simpa using leadingCoeff_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 leadingCoeff (Multiset.map f s.val)) ≠ 0
simpa using h