pow_eq_pow_mod — Mathlib

English

If a^n = 1, then for all m, a^m = a^{m mod n}.

Русский

Если a^n = 1, тогда для любого m выполняется a^m = a^{m mod n}.

LaTeX

$$$a^{n} = 1 \\Rightarrow a^{m} = a^{m \\bmod n}$$$

Lean4

/-- If `x ^ n = 1`, then `x ^ m` is the same as `x ^ (m % n)` -/
@[to_additive nsmul_eq_mod_nsmul /-- If `n • x = 0`, then `m • x` is the same as `(m % n) • x` -/
    ]
theorem pow_eq_pow_mod (m : ℕ) (ha : a ^ n = 1) : a ^ m = a ^ (m % n) := by
  calc
    a ^ m = a ^ (m % n + n * (m / n)) := by rw [Nat.mod_add_div]
    _ = a ^ (m % n) := by simp [pow_add, pow_mul, ha]

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