Theorems · Theorem · number theory

FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate

∀ (K : Type u_1) [inst : Field K] [inst_1 : Fintype K] (L : Type u_3) [inst_2 : Field L] [inst_3 : Algebra K L]
  [inst_4 : Algebra.IsAlgebraic K L] (n : ℕ),
  (⇑(FiniteField.frobeniusAlgEquivOfAlgebraic K L))^[n] = fun x => x ^ Fintype.card K ^ n

Defined in

Mathlib.FieldTheory.Finite.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFintypeFieldAlgebraAlgebra.IsAlgebraic