minpoly_eq_X_sub_C_pow — Mathlib

English

For a purely inseparable extension with q-th characteristic, the minimal polynomial of each x has the form (X - C x)^{q^n}.

Русский

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

LaTeX

$$$ \forall x:\, E, \exists n:\, \mathbb{N}, minpoly F x = (X - C x)^{q^n}$$$

Lean4

theorem minpoly_eq_X_sub_C_pow (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] (x : E) :
    ∃ n : ℕ, (minpoly F x).map (algebraMap F E) = (X - C x) ^ q ^ n :=
  (isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow F q).1 ‹_› x

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