Theorem: totient_of_prime (RSAProject/rsaproject.lean)

State before:
p : ℕ
hp : Nat.Prime p
⊢ Nat.totient p = p - 1
Tactic:
rw [Nat.totient_prime hp]
State after:
no goals