R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
⊢ prod (Multiset.map (↑leadingCoeffHom) t) = prod (Multiset.map (fun f => leadingCoeff f) t)
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
⊢ leadingCoeff (prod t) = prod (Multiset.map (fun f => leadingCoeff f) t)
rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]
no goals
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
⊢ prod (Multiset.map (↑leadingCoeffHom) t) = prod (Multiset.map (fun f => leadingCoeff f) t)
rfl