mathlib

b9387a48 - feat(data/nat/totient): lemmas `totient_mul_of_prime_of_{not_}dvd` (#15645)

feat(data/nat/totient): lemmas `totient_mul_of_prime_of_{not_}dvd` (#15645) Add `totient_mul_of_prime_of_not_dvd (hp : p.prime) (h : ¬ p ∣ n) : (p * n).totient = (p - 1) * n.totient` and golf `totient_mul_of_prime_of_dvd`.