pow_card_sub_one_eq_one — Mathlib

English

For a nonzero a ∈ ZMod p, a^{p-1} = 1.

Русский

Для непустого элемента a в ZMod p верно a^{p-1} = 1.

LaTeX

$$$a \\ne 0 \\Rightarrow a^{p-1} = 1 \\quad (a \\in \\mathbb{Z}/p\\mathbb{Z})$$$

Lean4

/-- **Fermat's Little Theorem**: for all nonzero `a : ZMod p`, we have `a ^ (p - 1) = 1`. -/
theorem pow_card_sub_one_eq_one {a : ZMod p} (ha : a ≠ 0) : a ^ (p - 1) = 1 :=
  by
  have h := FiniteField.pow_card_sub_one_eq_one a ha
  rwa [ZMod.card p] at h

Похожие утверждения