no goals
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hsplit : Splits (RingHom.id K) p
⊢ p = ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
simpa using eq_prod_roots_of_splits hsplit