English
Let F be a field of exponential characteristic q, E an extension with x ∈ E. The minimal polynomial minpoly F x has separable degree 1 if and only if it is of the form X^{q^n} − C y for some n ∈ N and y ∈ F.
Русский
Пусть F — поле характеристикой q в экспоненциальном смысле, E — над полем F, и x ∈ E. Мінімальный полином minpoly F x имеет разделительную степень 1 тогда и только тогда, когда он имеет вид X^{q^n} − C y для некоторого n ∈ N и y ∈ F.
LaTeX
$$$ (\minpoly F x).natSepDegree = 1 \iff \exists n \in \mathbb{N}, \exists y \in F, \ minpoly F x = X^{q^{n}} - C y $$$
Lean4
/-- The minimal polynomial of an element of `E / F` of exponential characteristic `q` has
separable degree one if and only if the minimal polynomial is of the form
`X ^ (q ^ n) - C y` for some `n : ℕ` and `y : F`. -/
theorem natSepDegree_eq_one_iff_eq_X_pow_sub_C :
(minpoly F x).natSepDegree = 1 ↔ ∃ (n : ℕ) (y : F), minpoly F x = X ^ q ^ n - C y := by
simp only [minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C q, map_sub, expand_X, expand_C]
