Theorems · Definition · field theory

IsPurelyInseparable.elemReduct

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

The element y of the base field K such that a ^ ringExpChar K ^ elemExponent K a = algebraMap K L y. See IsPurelyInseparable.algebraMap_elemReduct_eq.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Exponent

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsPurelyInseparable