units_pow_card_sub_one_eq_one — Mathlib

English

For every unit a ∈ (ZMod p)ˣ, we have a^{p-1} = 1.

Русский

Для любого элемента a из группы единиц ZMod p имеем a^{p-1} = 1.

LaTeX

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

Lean4

/-- **Fermat's Little Theorem**: for every unit `a` of `ZMod p`, we have `a ^ (p - 1) = 1`. -/
theorem units_pow_card_sub_one_eq_one (p : ℕ) [Fact p.Prime] (a : (ZMod p)ˣ) : a ^ (p - 1) = 1 := by
  rw [← card_units p, pow_card_eq_one]

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