Theorem: HTPI.Exercise_7_4_5_Nat (HTPILib/Chap7.lean)

State before:
m a n : ℕ
⊢ [↑a]_m ^ n = [↑a ^ n]_m
Tactic:
rewrite [Exercise_7_4_5_Int]
State after:
m a n : ℕ
⊢ [↑a ^ n]_m = [↑a ^ n]_m

State before:
m a n : ℕ
⊢ [↑a ^ n]_m = [↑a ^ n]_m
Tactic:
rfl
State after:
no goals