English
If there is a noncentral element a in D, there exists n ≥ 1 with a^(p^n) ∈ k and a power-based conjugacy property.
Русский
Если есть нецентральный элемент a в D, существует n ≥ 1 такое, что a^(p^n) ∈ k и выполняются доп. условия.
LaTeX
$$$\\exists n, 1 \\le n \\; \\wedge\\; a^{p^n} \\in k$$$
Lean4
/-- If `D` is a purely inseparable extension of `k` with characteristic `p`,
then for every element `a` of `D \ k`, there exists a natural number `n`
**greater than 0** such that `a ^ (p ^ n)` is contained in `k`. -/
theorem exists_pow_mem_center_of_inseparable' (p : ℕ) [ExpChar D p] {a : D} (ha : a ∉ k)
(hinsep : ∀ x : D, IsSeparable k x → x ∈ k) : ∃ n, 1 ≤ n ∧ a ^ (p ^ n) ∈ k :=
by
obtain ⟨n, hn⟩ := exists_pow_mem_center_of_inseparable p a hinsep
have nzero : n ≠ 0 := by
rintro rfl
rw [pow_zero, pow_one] at hn
exact ha hn
exact ⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩
