zpow_eq_zpow_emod — Mathlib

English

Let x ∈ G and integers m,n with x^n = 1. Then x^m = x^{m mod n}.

Русский

Пусть x ∈ G и целые m,n удовлетворяют x^n = 1. Тогда x^m = x^{m mod n}.

LaTeX

$$$\forall x \in G,\ \forall m,n \in \mathbb{Z},\ x^{n} = 1 \Rightarrow x^{m} = x^{m\bmod n}$$$

Lean4

theorem zpow_eq_zpow_emod {x : G} (m : ℤ) {n : ℤ} (h : x ^ n = 1) : x ^ m = x ^ (m % n) :=
  calc
    x ^ m = x ^ (m % n + n * (m / n)) := by rw [Int.emod_add_mul_ediv]
    _ = x ^ (m % n) := by simp [zpow_add, zpow_mul, h]

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