Theorems · Theorem · number theory

FiniteField.frobenius_pow

∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p : ℕ} [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP K p]
  {n : ℕ}, Fintype.card K = p ^ n → frobenius K p ^ n = 1

Defined in

Mathlib.FieldTheory.Finite.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFintypeFactCharP