strictMono_mersenne

Mathlib.NumberTheory.LucasLehmer

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

English

mersenne(n+1) = 2·mersenne(n) + 1.

Русский

mersenne(n+1) = 2·mersenne(n) + 1.

LaTeX

$$$$\mathrm{mersenne}(n+1)=2\cdot\mathrm{mersenne}(n)+1.$$$$

Lean4

theorem strictMono_mersenne : StrictMono mersenne := fun m n h ↦
  (Nat.sub_lt_sub_iff_right <| Nat.one_le_pow _ _ two_pos).2 <| by gcongr; norm_num1

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

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

Разделы

Аффилиация

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