p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ coprime p n
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n
rw [totient_mul _, totient_prime hp]
no goals
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ coprime p n
simpa [h] using coprime_or_dvd_of_prime hp n