r_one_pow_n

Mathlib.GroupTheory.SpecificGroups.Dihedral

URI: https://scilib.ai/kg/mathlib#DihedralGroup.r_one_pow_n

English

In the dihedral group of order 2n, the rotation element r by one step has order n; equivalently, r^n is the identity.

Русский

В диедральной группе порядка 2n вращение на один шаг обозначим как r; тогда у него порядок равен n, то есть r^n = e.

LaTeX

$$$r^n = 1$$$

Lean4

theorem r_one_pow_n : r (1 : ZMod n) ^ n = 1 := by simp

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

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

Разделы

Аффилиация

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