rw [pow_add, pow_one, pow_mul]
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message ^ (1 + totient (p * q) * k) % (p * q) = message * (message ^ totient (p * q)) ^ k % (p * q)
no goals