of_mersenne

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#Nat.Prime.of_mersenne

← MathLib Explorer

English

If 2^p − 1 is prime, then p is prime.

Русский

Если 2^p − 1 является простым числом, то p простое.

LaTeX

$$$\text{If } (2^p-1) \text{ is prime, then } p \text{ is prime.}$$$

Lean4

/-- If `2 ^ p - 1` is prime, then `p` is prime. -/
theorem of_mersenne {p : ℕ} (h : (mersenne p).Prime) : Nat.Prime p :=
  by
  apply Nat.prime_of_pow_sub_one_prime _ h |>.2
  rintro rfl
  apply Nat.not_prime_one h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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