no goals
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
⊢ leadingCoeff (∏ i in s, f i) = ∏ i in s, leadingCoeff (f i)
simpa using leadingCoeff_multiset_prod (s.1.map f)