feat(data/nat/pow): add theorem nat.pow_mod (#13551)

Add theorem that states `∀ (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n`.
leanprover-community · Apr 21, 2022 · afe1421 · afe1421
1 parent 090e59d
commit afe1421
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/data/nat/pow.lean b/src/data/nat/pow.lean
@@ -115,6 +115,12 @@ alias nat.sq_sub_sq ← nat.pow_two_sub_pow_two
 
 /-! ### `pow` and `mod` / `dvd` -/
 
+theorem pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n :=
+begin
+  induction b with b ih,
+  refl, simp [pow_succ, nat.mul_mod, ih],
+end
+
 theorem mod_pow_succ {b : ℕ} (w m : ℕ) :
   m % (b^succ w) = b * (m/b % b^w) + m % b :=
 begin