a_mul_xa

Mathlib.GroupTheory.SpecificGroups.Quaternion

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

English

In QuaternionGroup, the product of a and xa satisfies a_i xa_j = xa_{j - i}.

Русский

В QuaternionGroup произведение a_i и xa_j равно xa_{j - i}.

LaTeX

$$$a_i \cdot xa_j = xa_{\,j - i}$$$

Lean4

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

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

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

Разделы

Аффилиация

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