Theorems · Theorem · field theory

isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow

∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q],
  IsPurelyInseparable F E ↔
    ∀ (x : E), ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n

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.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Basic

Cited by

1 results in Mathlib

Foundations

Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraExpChar