isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C

English

For a purely inseparable extension with characteristic q, every x ∈ E has n,y ∈ ℕ, F with minpoly F x = X^{q^n} - C y.

Русский

При чисто безразделимом расширении характеристики q каждый элемент x ∈ E имеет числа n∈ℕ и y∈F такие, что minpoly_F(x) = X^{q^n} - C y.

LaTeX

$$(∀ x ∈ E) ∃ n ∈ ℕ, ∃ y ∈ F, minpoly F x = X^{q^n} - C y$$

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 ^ (q ^ n) - y` for some natural number `n` and some element `y` of `F`. -/
theorem isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C (q : ℕ) [hF : ExpChar F q] :
    IsPurelyInseparable F E ↔ ∀ x : E, ∃ (n : ℕ) (y : F), minpoly F x = X ^ q ^ n - C y := by
  simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one, minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q]

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