α

Mathlib.NumberTheory.LucasLehmer

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

English

α is defined as the pair (0,1) in X_q, representing √3.

Русский

α определяется как пара (0,1) в X_q, соответствующая √3.

LaTeX

$$$ \alpha : X q =\; (0, 1) $$$

Lean4

/-- We define `α = √3`. -/
def α : X q :=
  (0, 1)

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

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

Разделы

Аффилиация

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