r_one_pow

Mathlib.GroupTheory.SpecificGroups.Dihedral

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

English

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

Русский

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

LaTeX

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

Lean4

theorem r_one_pow (k : ℕ) : (r 1 : DihedralGroup n) ^ k = r k := by simp only [r_pow, one_mul]

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

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

Разделы

Аффилиация

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