pow): add theorem `nat.pow_mod` (#13551)

Commit

3 years ago

feat(data/nat/pow): add theorem `nat.pow_mod` (#13551) Add theorem that states `∀ (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n`.

Author

slerpyyy

Parents