Modular exponentiation with the totient function

This file contains lemmas about modular exponentiation. In particular, it contains lemmas showing that an exponent can be reduced modulo the totient function when the base is coprime to the modulus.

Main Results

• pow_totient_mod: If x is coprime to n, then the modular exponentiation x ^ k % n can be reduced to x ^ (k % φ n) % n.

TODOs

• Extend to results in cases where the base is not coprime to the modulus.
• Write a tactic or simproc that can automatically reduce exponents or towers of exponents using these results.

theorem Nat.pow_totient_mod_eq_one {x n : ℕ} (hn : 1 < n) (h : x.Coprime n) : x ^ n.totient % n = 1

theorem Nat.pow_add_totient_mod_eq {x k n : ℕ} (hn : 1 < n) (h : x.Coprime n) : x ^ (k + n.totient) % n = x ^ k % n

theorem Nat.pow_add_mul_totient_mod_eq {x k l n : ℕ} (hn : 1 < n) (h : x.Coprime n) : x ^ (k + l * n.totient) % n = x ^ k % n

theorem Nat.pow_totient_mod {x k n : ℕ} (hn : 1 < n) (h : x.Coprime n) : x ^ k % n = x ^ (k % n.totient) % n