r_pow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem r_pow (i : ZMod n) (k : ℕ) : (r i) ^ k = r (i * k : ZMod n) := by
  induction k with
  | zero => simp only [pow_zero, Nat.cast_zero, mul_zero, r_zero]
  | succ k IH => rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]

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