instMul

Mathlib.NumberTheory.LucasLehmer

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

English

Multiplication on X_q is defined by (a,b)·(c,d) = (ac + 3bd, ad + bc).

Русский

Умножение на X_q задаётся как (a,b)·(c,d) = (ac + 3bd, ad + bc).

LaTeX

$$$ (x,y) \cdot (u,v) = (x u + 3 y v, x v + y u) $$$

Lean4

instance : Mul (X q) where mul x y := (x.1 * y.1 + 3 * x.2 * y.2, x.1 * y.2 + x.2 * y.1)

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

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

Разделы

Аффилиация

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