Theorems · Theorem · field theory

IsPurelyInseparable.algebraMap_iterateFrobenius

∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [inst_4 : ExpChar K p] {n : ℕ}
  (hn : IsPurelyInseparable.exponent K L ≤ n) (a : L),
  (algebraMap K L) ((IsPurelyInseparable.iterateFrobenius K L p hn) a) = a ^ p ^ n

Action of iterateFrobenius on the top field.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Exponent

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsPurelyInseparable.HasExponentExpChar