succ_mersenne

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#succ_mersenne

English

For every natural k, the Mersenne number satisfies M_k + 1 = 2^k.

Русский

Для любого натурального k число Мерсенна M_k равно 2^k − 1, значит M_k + 1 = 2^k.

LaTeX

$$$(2^k - 1) + 1 = 2^k$$$

Lean4

@[simp]
theorem succ_mersenne (k : ℕ) : mersenne k + 1 = 2 ^ k :=
  by
  rw [mersenne, tsub_add_cancel_of_le]
  exact one_le_pow₀ (by simp)

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

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

Разделы

Аффилиация

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