α_sq

Mathlib.NumberTheory.LucasLehmer

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

English

α^2 = 3 in X_q.

Русский

α^2 = 3 в X_q.

LaTeX

$$$ \alpha^2 = 3 $$$

Lean4

@[simp]
theorem α_sq : (α ^ 2 : X q) = 3 := by ext <;> simp [α, sq]

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

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

Разделы

Аффилиация

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