p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (gcd p n) * φ (p * n) = φ p * φ n * gcd p n
⊢ φ (p * n) = p * φ n
p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n
have h1 := totient_gcd_mul_totient_mul p n
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (gcd p n) * φ (p * n) = φ p * φ n * gcd p n
⊢ φ (p * n) = p * φ n
rw [gcd_eq_left h, mul_assoc] at h1
no goals
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ p * φ (p * n) = φ p * (φ n * p)
⊢ φ (p * n) = p * φ n
simpa [(totient_pos hp.pos).ne', mul_comm] using h1