isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow

English

A field extension is purely inseparable iff for every element x, the minimal polynomial has natSepDegree equal to 1.

Русский

Расширение поля чисто безразделимо тогда и только тогда, когда для каждого элемента x минимальный многочлен имеет natSepDegree равную 1.

LaTeX

$$$ IsPurelyInseparable F E \iff \forall x:\, E, (minpoly F x).natSepDegree = 1 $$$

Lean4

/-- A field extension `E / F` of exponential characteristic `q` is purely inseparable
if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form
`(X - x) ^ (q ^ n)` for some natural number `n`. -/
theorem isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow (q : ℕ) [hF : ExpChar F q] :
    IsPurelyInseparable F E ↔ ∀ x : E, ∃ n : ℕ, (minpoly F x).map (algebraMap F E) = (X - C x) ^ q ^ n := by
  simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one, minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow q]

Похожие утверждения