English
Definition: An element x of an algebra K over F is separable if its minimal polynomial over F is separable.
Русский
Определение: элемент x алгебры K над F является разделяемым, если его минимальный многочлен над F разделим.
LaTeX
$$IsSeparable(F x) := Separable(minpoly F x)$$
Lean4
/-- An element `x` of an algebra `K` over a commutative ring `F` is said to be *separable*, if its
minimal polynomial over `K` is separable. Note that the minimal polynomial of any element not
integral over `F` is defined to be `0`, which is not a separable polynomial.
-/
@[stacks 09H1 "second part"]
def IsSeparable (x : K) : Prop :=
Polynomial.Separable (minpoly F x)
