Theorems · Theorem · field theory

isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C

∀ (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 y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y

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.

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