Theorems · Definition · field theory

IsPurelyInseparable.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 : ℕ) → [ExpChar K p] → {n : ℕ} → IsPurelyInseparable.exponent K L ≤ n → L →+* K

Iterated Frobenius map (ring homomorphism) for purely inseparable field extension with exponent. If n ≥ exponent K L, it acts like x ↦ x ^ p ^ n but the codomain is the base field K.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Exponent

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraIsPurelyInseparable.HasExponentExpChar