α_pow

Mathlib.NumberTheory.LucasLehmer

URI: https://scilib.ai/kg/mathlib#LucasLehmer.X.α_pow

English

For all i, α^{2i+1} = 3^i α.

Русский

Для всех i выполняется α^{2i+1} = 3^i α.

LaTeX

$$$ \alpha^{2i+1} = 3^i \alpha $$$

Lean4

theorem α_pow (i : ℕ) : (α : X q) ^ (2 * i + 1) = 3 ^ i * α := by rw [pow_succ, pow_mul, α_sq]

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

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

Разделы

Аффилиация

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