a_one_pow_n

Mathlib.GroupTheory.SpecificGroups.Quaternion

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

English

The element a_1 has order 2n; in particular, a_1^(2n) = 1.

Русский

Элемент a_1 имеет порядок 2n; в частности, a_1^(2n) = 1.

LaTeX

$$$a_1^{2n} = 1$$$

Lean4

theorem a_one_pow_n : (a 1 : QuaternionGroup n) ^ (2 * n) = 1 := by simp

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

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

Разделы

Аффилиация

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