English
Let F be a field and p ∈ F[X] separable that splits in K over F. Then the number of distinct roots of p in K equals the degree of p, i.e., |p.rootSet(K)| = natDegree(p).
Русский
Пусть F — поле и p ∈ F[X] разделимая над F и раскладывается в поле K. Тогда число различных корней p в K равно степени p, т.е. |p.rootSet(K)| = natDegree(p).
LaTeX
$$$\\text{If } p \\text{ is separable and splits over } K, \\; |p.{rootSet}(K)| = p.natDegree$$$
Lean4
theorem card_rootSet_eq_natDegree [Algebra F K] {p : F[X]} (hsep : p.Separable) (hsplit : Splits (algebraMap F K) p) :
Fintype.card (p.rootSet K) = p.natDegree := by
classical
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← natDegree_eq_card_roots hsplit]
