Mathlib Map

Theorems · Theorem · number theory

ZMod.pow_card

∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (x : ZMod p), x ^ p = x

A variation on Fermat's little theorem. See ZMod.pow_card_sub_one_eq_one

Defined in
Mathlib.FieldTheory.Finite.Basic
Cited by
5 results in Mathlib
Foundations
Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Fact
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ZMod.pow_card_pow · cited by 1ZMod.pow_card_powInt.ModEq.pow_prime_eq_self · cited by 1ModEq.pow_prime_eq_selfWittVector.frobenius_zmodp · cited by 1WittVector.frobenius_zmodpMvPolynomial.frobenius_zmod · cited by 1MvPolynomial.frobenius_zm…ZMod.frobenius_zmod · cited by 0ZMod.frobenius_zmodFact · cited by 2726FactNat.Prime · cited by 2059Nat.PrimeFintype.card · cited by 1386Fintype.cardZMod · cited by 1024ZModZMod.card · cited by 36ZMod.cardFiniteField.pow_card · cited by 8FiniteField.pow_cardZMod.pow_cardCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.