English
Let f ∈ F[X] be nonzero and split over F. Then f has no repeated roots if and only if f is separable.
Русский
Пусть f ∈ F[X] не равно нулю и раскладывается над F. Тогда у f нет повторяющихся корней тогда и только тогда, когда f разделимо (separable).
LaTeX
$$$f \\neq 0 \\land f.Splits (\\mathrm{id}_F) \\Rightarrow (f.roots.Nodup \\iff f.Separable)$$$
Lean4
/-- If a non-zero polynomial splits, then it has no repeated roots on that field
if and only if it is separable. -/
theorem nodup_roots_iff_of_splits {f : F[X]} (hf : f ≠ 0) (h : f.Splits (RingHom.id F)) : f.roots.Nodup ↔ f.Separable :=
by
classical
refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
obtain ⟨x, hx⟩ := exists_root_of_splits _ (splits_of_splits_of_dvd _ hf h (gcd_dvd_left f _)) hnsep
simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
