mersenne_odd

Mathlib.NumberTheory.LucasLehmer

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

← MathLib Explorer

English

For all p, mersenne(p) is odd if and only if p ≠ 0.

Русский

Для любого p число mersenne(p) нечётно тогда и только тогда, когда p ≠ 0.

LaTeX

$$$\text{Odd}(\text{mersenne}(p)) \iff p \neq 0$$$

Lean4

@[simp]
theorem mersenne_odd : ∀ {p : ℕ}, Odd (mersenne p) ↔ p ≠ 0
  | 0 => by simp
  | p + 1 => by simpa using Nat.Even.sub_odd (one_le_pow₀ one_le_two) (even_two.pow_of_ne_zero p.succ_ne_zero) odd_one

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

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

Разделы

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

Аффилиация

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