mersenne_lt_mersenne

Mathlib.NumberTheory.LucasLehmer

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

English

If mersenne(p) is prime, then p is prime.

Русский

Если mersenne(p) простое, то p является простым.

LaTeX

$$$$\text{If } \mathrm{mersenne}(p) \text{ is prime, then } p \text{ is prime}.$$$$

Lean4

@[simp]
theorem mersenne_lt_mersenne {p q : ℕ} : mersenne p < mersenne q ↔ p < q :=
  strictMono_mersenne.lt_iff_lt

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

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

Разделы

Аффилиация

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