pow_card_sub_one_sub_one_mod_card

English

For prime p and coprime n, (n^{p-1} − 1) ≡ 0 (mod p).

Русский

Для простого p и взаимно простого n, (n^{p-1} − 1) ≡ 0 (mod p).

LaTeX

$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, \\\\gcd(n,p)=1 \\\\Rightarrow (n^{(p-1)} - 1) \\\\equiv 0 \\\\pmod p$$$

Lean4

/-- **Fermat's Little Theorem**: for all `n : ℕ` coprime to `p`, we have
`(n ^ (p - 1) - 1) % p = 0`. -/
theorem pow_card_sub_one_sub_one_mod_card {p : ℕ} (hp : p.Prime) {n : ℕ} (hpn : n.Coprime p) :
    (n ^ (p - 1) - 1) % p = 0 :=
  Nat.sub_mod_eq_zero_of_mod_eq (Nat.ModEq.pow_card_sub_one_eq_one hp hpn)

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