a_mul_a

Mathlib.GroupTheory.SpecificGroups.Quaternion

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

English

In QuaternionGroup, the product of two a-elements corresponds to addition of their indices modulo 2n: a_i a_j = a_{i+j}.

Русский

В QuaternionGroup произведение элементов типа a соответствует сложению индексов по модулю 2n: a_i a_j = a_{i+j}.

LaTeX

$$$a_i a_j = a_{i+j}$$$

Lean4

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

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

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

Разделы

Аффилиация

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