pow_card_sub_one_eq_one — Mathlib

English

Under suitable divisibility and positivity conditions, n^x ≡ n^y (mod p) for integers n and prime p.

Русский

При подходящих условиях делимости и положительности выполняется n^x ≡ n^y (mod p).

LaTeX

$$$\\\\forall p,x,y \\\\in \\\\mathbb{N}, \\\\text{Prime}(p) \\\\Rightarrow \\\\text{divisor}(p-1, x-y) \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{Z}, n^{x} \\\\equiv n^{y} \\\\pmod p$$$

Lean4

/-- **Fermat's Little Theorem**: for all `n : ℕ` coprime to `p`, we have
`n ^ (p - 1) ≡ 1 [MOD p]`. -/
theorem pow_card_sub_one_eq_one {p : ℕ} (hp : p.Prime) {n : ℕ} (hpn : n.Coprime p) : n ^ (p - 1) ≡ 1 [MOD p] :=
  by
  rw [← Int.natCast_modEq_iff, Nat.cast_pow, Nat.cast_one]
  exact Int.ModEq.pow_card_sub_one_eq_one hp (isCoprime_iff_coprime.mpr hpn)

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