English
If every element of K is separable over F, then every element of K is algebraic over F.
Русский
Если каждый элемент K над F разделим, то каждый элемент K над F алгебраичен.
LaTeX
$$IsSeparable F K ⇒ ∀ x ∈ K, Algebra.IsAlgebraic F x$$
Lean4
/-- If the minimal polynomial of `x : K` over `F` is separable, then `x` is integral over `F`,
because the minimal polynomial of a non-integral element is `0`, which is not separable. -/
theorem isIntegral {x : K} (h : IsSeparable F x) : IsIntegral F x :=
by
cases subsingleton_or_nontrivial F
· haveI := Module.subsingleton F K
exact ⟨1, monic_one, Subsingleton.elim _ _⟩
· exact of_not_not (h.ne_zero <| minpoly.eq_zero ·)
