∀ (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], ⇑(FiniteField.frobeniusAlgEquivOfAlgebraic K L) = fun x => x ^ Fintype.card K