r_zpow

Mathlib.GroupTheory.SpecificGroups.Dihedral

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

English

For i ∈ ZMod n and k ∈ Z, (r i)^{k} = r(i k).

Русский

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

LaTeX

$$$(r_i)^{k} = r_{i k} \quad (i \in ZMod\ n, k \in \mathbb Z)$$$

Lean4

@[simp]
theorem r_zpow (i : ZMod n) (k : ℤ) : (r i) ^ k = r (i * k : ZMod n) := by cases k <;> simp [r_pow, neg_mul_eq_mul_neg]

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

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

Разделы

Аффилиация

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