prime_dvd_pow_self_sub

Mathlib.FieldTheory.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Int.prime_dvd_pow_self_sub

English

For prime p and integer n, p divides n^p − n.

Русский

Для простого p и целого n, p делит n^p − n.

LaTeX

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

Lean4

theorem prime_dvd_pow_self_sub {p : ℕ} (hp : Nat.Prime p) (n : ℤ) : (p : ℤ) ∣ n ^ p - n :=
  (ModEq.pow_prime_eq_self hp n).symm.dvd

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru