Theorems · Theorem · ring theory

JacobsonNoether.exists_pow_mem_center_of_inseparable

∀ {D : Type u_1} [inst : DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [hchar : ExpChar D p]
  (a : D), (∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) → ∃ n, a ^ p ^ n ∈ Subring.center D

If D is a purely inseparable extension of k with characteristic p, then for every element a of D, there exists a natural number n such that a ^ (p ^ n) is contained in k.

Defined in

Mathlib.FieldTheory.JacobsonNoether

Cited by

2 results in Mathlib

Foundations

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

Assumes

DivisionRingAlgebra.IsAlgebraicExpChar