F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ card (Multiset.toFinset (roots (map (algebraMap F K) p))) = natDegree p
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ Fintype.card ↑(rootSet p K) = natDegree p
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ Multiset.Nodup (roots (map (algebraMap F K) p))
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ card (Multiset.toFinset (roots (map (algebraMap F K) p))) = natDegree p
rw [Multiset.toFinset_card_of_nodup, ← natDegree_eq_card_roots hsplit]
no goals
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
p : F[X]
hsep : Separable p
hsplit : Splits (algebraMap F K) p
⊢ Multiset.Nodup (roots (map (algebraMap F K) p))
exact nodup_roots hsep.map