pow_prime_eq_self — Mathlib

English

For every prime p and integer n, n^p ≡ n (mod p).

Русский

Для каждого простого p и целого n верно n^p ≡ n (mod p).

LaTeX

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

Lean4

theorem pow_prime_eq_self {p : ℕ} (hp : Nat.Prime p) (n : ℤ) : n ^ p ≡ n [ZMOD p] :=
  by
  haveI : Fact p.Prime := ⟨hp⟩
  simp [← ZMod.intCast_eq_intCast_iff]

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