r_one_zpow

Mathlib.GroupTheory.SpecificGroups.Dihedral

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

English

For k ∈ Z, (r 1)^{k} = r k.

Русский

Для k ∈ Z выполняется (r 1)^{k} = r k.

LaTeX

$$$(r_1)^k = r_k \quad (k \in \mathbb Z)$$$

Lean4

theorem r_one_zpow (k : ℤ) : (r 1 : DihedralGroup n) ^ k = r k := by simp only [r_zpow, one_mul]

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

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

Разделы

Аффилиация

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