English
Let f be a polynomial over a field F. Then the separable degree of f over F equals the number of distinct roots of f in any algebraic closure, i.e., over an algebraically closed field E, natSepDegree(f) equals the cardinality of the finite set of distinct roots of f in E.
Русский
Пусть f — многочлен над полем F. Тогда разделяемая степень f над F равна числу различных корней f в любом алгебраически замкнутом разширении; то есть над полем E, natSepDegree(f) равно числу различных корней f в E.
LaTeX
$$$ \operatorname{natSepDegree}(f) = \#\big((f.\aroots E).toFinset\big)$$$
Lean4
/-- The separable degree of a polynomial is equal to
the number of distinct roots of it over any algebraically closed field. -/
theorem natSepDegree_eq_of_isAlgClosed [DecidableEq E] [IsAlgClosed E] : f.natSepDegree = (f.aroots E).toFinset.card :=
natSepDegree_eq_of_splits f (IsAlgClosed.splits_codomain f)
