English
Let F and K be fields and f ∈ F[X] with f ≠ 0. If f splits over K (via the map F → K), then the set of roots of f in K is without repetition if and only if f is separable.
Русский
Пусть F и K — поля, f ∈ F[X] не нулевой. Если f распадается над K через отображение F → K, то множество корней f в K без повторов эквивалентно тому, что f разделимо.
LaTeX
$$$ f \\neq 0 \\land f.Splits (\\mathrm{algebraMap} F K) \\Rightarrow (f.aroots K).Nodup \\iff f.Separable $$$
Lean4
/-- If a non-zero polynomial over `F` splits in `K`, then it has no repeated roots on `K`
if and only if it is separable. -/
@[stacks 09H3 "Here we only require `f` splits instead of `K` is algebraically closed."]
theorem nodup_aroots_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0) (h : f.Splits (algebraMap F K)) :
(f.aroots K).Nodup ↔ f.Separable :=
by
rw [← (algebraMap F K).id_comp, ← splits_map_iff] at h
rw [nodup_roots_iff_of_splits (map_ne_zero hf) h, separable_map]
