Simple roots are separable

An element y of a field extension of K that is a simple root of some polynomial p over K, that is p(y) = 0 and p′(y) ≠ 0, is separable over K: writing p = minpoly · r, the derivative p′(y) = minpoly′(y) r(y) is nonzero, so minpoly′ ≠ 0. Consequently a field generated over K by such an element is finite and separable over K.

Main results

• TauCeti.isSeparable_of_aeval_derivative_ne_zero: a simple root of a polynomial is separable.
• TauCeti.finiteDimensional_and_isSeparable_of_aeval_derivative_ne_zero: a field generated by a simple root of a polynomial is finite and separable.

theorem TauCeti.isSeparable_of_aeval_derivative_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : Polynomial K} {y : L} (hp : (Polynomial.aeval y) p = 0) (hd : (Polynomial.aeval y) (Polynomial.derivative p) ≠ 0) : IsSeparable K y

A simple root is separable: if p(y) = 0 and p′(y) ≠ 0, then y is separable.

theorem TauCeti.finiteDimensional_and_isSeparable_of_aeval_derivative_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {p : Polynomial K} {y : L} (hgen : K⟮y⟯ = ⊤) (hp : (Polynomial.aeval y) p = 0) (hd : (Polynomial.aeval y) (Polynomial.derivative p) ≠ 0) : FiniteDimensional K L ∧ Algebra.IsSeparable K L

A field generated by a simple root is finite and separable: if L = K⟮y⟯, where p(y) = 0 and p′(y) ≠ 0, then L / K is finite and separable.