English
For an irreducible polynomial f over a field, f is separable if and only if its derivative is nonzero.
Русский
Для ирредуцируемого многочлена f над полем выполнено: f сепарабелен тогда и только тогда, когда производная не равна нулю.
LaTeX
$$$ \text{Irreducible}(f) \Rightarrow (\operatorname{Separable}(f) \iff \operatorname{derivative}(f) \neq 0)$$$
Lean4
theorem separable_iff_derivative_ne_zero {f : F[X]} (hf : Irreducible f) : f.Separable ↔ derivative f ≠ 0 :=
⟨fun h1 h2 => hf.not_isUnit <| isCoprime_zero_right.1 <| h2 ▸ h1, fun h =>
EuclideanDomain.isCoprime_of_dvd (mt And.right h) fun g hg1 _hg2 ⟨p, hg3⟩ hg4 =>
let ⟨u, hu⟩ := (hf.isUnit_or_isUnit hg3).resolve_left hg1
have : f ∣ derivative f := by
conv_lhs => rw [hg3, ← hu]
rwa [Units.mul_right_dvd]
not_lt_of_ge (natDegree_le_of_dvd this h) <| natDegree_derivative_lt <| mt derivative_of_natDegree_zero h⟩
