Theorems · Theorem · field theory

isPurelyInseparable_iff_pow_mem

∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ)
  [ExpChar F q], IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

A field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, there exists a natural number n such that x ^ (q ^ n) is contained in F.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

FieldRingIsDomainAlgebraExpChar