English
For a ∈ ZMod n and m ∈ ℕ with 1 < n, (a^m).val equals a.val^m provided appropriate modulus conditions; more generally, the equality holds when a.val^m < n so no wrap occurs.
Русский
Пусть a ∈ ZMod n и m ∈ ℕ, при n > 1 выполняется (a^m).val = a.val^m при отсутствии переполнения по модулю.
LaTeX
$$$ (a^m).val = a.val^m $$$
Lean4
theorem val_pow {m n : ℕ} {a : ZMod n} [ilt : Fact (1 < n)] (h : a.val ^ m < n) : (a ^ m).val = a.val ^ m := by
induction m with
| zero => simp [ZMod.val_one]
| succ m
ih =>
have : a.val ^ m < n := by
obtain rfl | ha := eq_or_ne a 0
· by_cases hm : m = 0
· cases hm; simp [ilt.out]
· simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
· exact lt_of_le_of_lt (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]
