Theorems · Theorem · field theory

IsPurelyInseparable.iterateFrobenius_algebraMap

∀ {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 : K),
  (IsPurelyInseparable.iterateFrobenius K L p hn) ((algebraMap K L) a) = a ^ p ^ n

Action of iterateFrobenius on the bottom field.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Exponent

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsPurelyInseparable.HasExponentExpChar