Theorems · Definition · field theory

IsPurelyInseparable.elemExponent

(K : Type u_2) →
  {L : Type u_3} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → [IsPurelyInseparable K L] → L → ℕ

The exponent of an element a ∈ L of a purely inseparable field extension L / K is the smallest natural number e such that a ^ ringExpChar K ^ e ∈ K.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Exponent

Cited by

15 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsPurelyInseparable