Euler_Phi_Function_of_Product_with_Prime
Provedeuler-phi-functionnumber-theoryproofwiki
Let p be prime and n >= 1. If p does not divide n, then phi(pn) = (p-1)*phi(n).
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Totient
Formal statement
theorem Euler_Phi_Function_of_Product_with_Prime (p n : ℕ) (hp : Nat.Prime p) (hn : 0 < n) (hpn : ¬ p ∣ n) : Nat.totient (p * n) = (p - 1) * Nat.totient n := by sorry
Source