Theorems · Theorem · number theory
FiniteField.pow_card
∀ {K : Type u_1} [inst : GroupWithZero K] [inst_1 : Fintype K] (a : K), a ^ Fintype.card K = a- Defined in
- Mathlib.FieldTheory.Finite.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZeroFintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- one_mulproof · cited by 2,841
- Fintype.cardstatement and proof · cited by 1,386
- GroupWithZerostatement and proof · cited by 691
- pow_succproof · cited by 374
- zero_powproof · cited by 361
- Fintype.card_posproof · cited by 31
- Fintype.card_ne_zeroproof · cited by 16
- FiniteField.pow_card_sub_one_eq_oneproof · cited by 7
Cited by8
Results whose statement or proof uses this declaration.
- ZMod.pow_cardproof · cited by 5
- FiniteField.orderOf_frobeniusAlgHomproof · cited by 3
- FiniteField.roots_X_pow_card_sub_Xproof · cited by 2
- FiniteField.frobenius_powproof · cited by 1
- FiniteField.trace_pow_cardproof · cited by 1
- IsArithFrobAt.exists_of_isInvariantproof · cited by 1
- Irreducible.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_Xproof · cited by 0
- FiniteField.pow_card_powproof · cited by 0