@[extern lean_nat_powmod]

def Nat.powMod (b e m : Nat) : Nat

Computes b ^ e % m by square-and-multiply, reducing modulo m at each step so that no intermediate value exceeds the square of the larger of b and m.

Because Nat.mod satisfies n % 0 = n, powMod b e 0 is b ^ e. That case is the exception to the bound above: there the intermediates are as large as the result.

powMod is not definitionally equal to b ^ e % m. Concrete exponents reduce in O(log e) steps under decide, which b ^ e % m could not, and simp evaluates closed terms with the Nat.reducePowMod simproc. For symbolic reasoning, rewrite with powMod_def, which is deliberately not @[simp]: it would turn a cheap powMod goal into an intractable b ^ e % m one.

Examples:

• powMod 3 4 5 = 1
• powMod 2 10 1000 = 24
• powMod 3 4 0 = 81

Equations

• b.powMod e m = if e = 0 then 1 % m else have r := (b * b % m).powMod (e / 2) m; if e % 2 = 1 then r * b % m else r

theorem Nat.powMod_def (b e m : Nat) : b.powMod e m = b ^ e % m

theorem Nat.powMod_zero (b m : Nat) : b.powMod 0 m = 1 % m

theorem Nat.powMod_succ (b e m : Nat) : b.powMod (e + 1) m = b.powMod e m * b % m

Not @[simp]: it would expand a numeric exponent into repeated multiplication.