English
In any field F, the polynomial X^n − 1 is separable if and only if n is nonzero in F (equivalently p ∤ n where p = char F).
Русский
В любом поле F многочлен X^n − 1 разделим тогда и только тогда, когда образ n в F не равен нулю (то есть p ∤ n, где p = char F).
LaTeX
$$$\\operatorname{Separable}(X^n - 1) \\iff (n : F) \\neq 0$$$
Lean4
/-- In a field `F`, `X ^ n - 1` is separable iff `↑n ≠ 0`. -/
theorem X_pow_sub_one_separable_iff {n : ℕ} : (X ^ n - 1 : F[X]).Separable ↔ (n : F) ≠ 0 :=
by
refine ⟨?_, fun h => separable_X_pow_sub_C_unit 1 (IsUnit.mk0 _ h)⟩
rw [separable_def', derivative_sub, derivative_X_pow, derivative_one, sub_zero]
-- Suppose `(n : F) = 0`, then the derivative is `0`, so `X ^ n - 1` is a unit, contradiction.
rintro (h : IsCoprime _ _) hn'
rw [hn', C_0, zero_mul, isCoprime_zero_right] at h
exact not_isUnit_X_pow_sub_one F n h
