English
If a polynomial splits over E, then its separable degree equals the number of distinct roots in E.
Русский
Если многочлен распадается в E, то его сепарабельная степень равна числу различных корней в E.
LaTeX
$$\( f.Splits (algebraMap F E) \Rightarrow f.natSepDegree = (f.aroots E).toFinset.card \)$$
Lean4
/-- If a polynomial splits over `E`, then its separable degree is equal to
the number of distinct roots of it over `E`. -/
theorem natSepDegree_eq_of_splits [DecidableEq E] (h : f.Splits (algebraMap F E)) :
f.natSepDegree = (f.aroots E).toFinset.card := by
classical
rw [aroots, ← (SplittingField.lift f h).comp_algebraMap, ← map_map,
roots_map _ ((splits_id_iff_splits _).mpr <| SplittingField.splits f), Multiset.toFinset_map,
Finset.card_image_of_injective _ (RingHom.injective _), natSepDegree]
