Theorems · Theorem · ring theory

JacobsonNoether.exist_pow_eq_zero_of_le

∀ {D : Type u_1} [inst : DivisionRing D] [Algebra.IsAlgebraic (↥(Subring.center D)) D] (p : ℕ) [hchar : ExpChar D p]
  {a : D},
  a ∉ Subring.center D →
    (∀ (x : D), IsSeparable (↥(Subring.center D)) x → x ∈ Subring.center D) →
      ∃ m, 1 ≤ m ∧ ∀ (n : ℕ), p ^ m ≤ n → (⇑((LieAlgebra.ad (↥(Subring.center D)) D) a))^[n] = 0

If D is a purely inseparable extension of k of characteristic p, then for every element a of D \ k, there exists a natural number m greater than 0 such that (a * x - x * a) ^ n = 0 (as linear maps) for every n greater than (p ^ m).

Defined in

Mathlib.FieldTheory.JacobsonNoether

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRingAlgebra.IsAlgebraicExpChar