xa_mul_xa

Mathlib.GroupTheory.SpecificGroups.Quaternion

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

English

In QuaternionGroup, xa_i xa_j equals a_{n + j - i}.

Русский

В QuaternionGroup xa_i xa_j = a_{n + j - i}.

LaTeX

$$$xa_i xa_j = a_{n + j - i}$$$

Lean4

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

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

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

Разделы

Аффилиация

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