Theorems · Theorem · field theory

IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem

∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q]
  {x : E}, IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

If F is of exponential characteristic q, then F⟮x⟯ / F is a purely inseparable extension if and only if x ^ (q ^ n) is contained in F for some n : ℕ.

Defined in

Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraExpChar