xa_mul_a

Mathlib.GroupTheory.SpecificGroups.Quaternion

URI: https://scilib.ai/kg/mathlib#QuaternionGroup.xa_mul_a

English

In QuaternionGroup, the product of xa_i and a_j equals xa_{i+j}.

Русский

Xa-переменная умножает a: xa_i a_j = xa_{i+j}.

LaTeX

$$$xa_i a_j = xa_{i+j}$$$

Lean4

@[simp]
theorem xa_mul_a (i j : ZMod (2 * n)) : xa i * a j = xa (i + j) :=
  rfl

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

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

Разделы

Аффилиация

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