∀ (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