minpoly_eq_X_pow_sub_C — Mathlib

English

For a purely inseparable extension with q-th characteristic, the minimal polynomial of each x has the form (X - Cx)^{q^n} when mapped into the base field.

Русский

Для чисто безразделимого расширения характеристика q имеет вид minpoly_F(x) = (X - C x)^{q^n} после отображения в основание.

LaTeX

$$[IsPurelyInseparable F E] (x ∈ E) ⇒ ∃ n ∈ ℕ, minpoly F x = X^{q^n} - C x$$

Lean4

theorem minpoly_eq_X_pow_sub_C (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] (x : E) :
    ∃ (n : ℕ) (y : F), minpoly F x = X ^ q ^ n - C y :=
  (isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C F q).1 ‹_› x

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