no goals
F : Type u
K : Type v
L : Type w
inst✝² : CommRing K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
p_ne_zero : map i p ≠ 0
hsplit : Splits i p
⊢ degree (map i p) = ↑(↑Multiset.card (roots (map i p)))
simp [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots' hsplit]