xa_sq

Mathlib.GroupTheory.SpecificGroups.Quaternion

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

English

For any i, (xa_i)^2 = a_n.

Русский

Для любого i: (xa_i)^2 = a_n.

LaTeX

$$$(xa_i)^2 = a_n$$$

Lean4

@[simp]
theorem xa_sq (i : ZMod (2 * n)) : xa i ^ 2 = a n := by simp [sq]

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

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

Разделы

Аффилиация

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