one_add_α_sq

Mathlib.NumberTheory.LucasLehmer

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

English

(1 + α)^2 = 2 ω in X_q.

Русский

(1 + α)^2 = 2 ω в X_q.

LaTeX

$$$ (1 + \alpha)^2 = 2 \omega $$$

Lean4

@[simp]
theorem one_add_α_sq : ((1 + α) ^ 2 : X q) = 2 * ω := by ext <;> simpa [α, ω, sq] using by norm_num

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

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

Разделы

Аффилиация

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