instOne

Mathlib.NumberTheory.LucasLehmer

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

English

The multiplicative identity is (1,0).

Русский

Единица умножения равна (1,0).

LaTeX

$$$1_{X_q} = (1,0)$$$

Lean4

instance : One (X q) where one := ⟨1, 0⟩

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

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

Разделы

Аффилиация

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