mathlib

7c205ffb - feat(data/nat/totient): add lemma `totient_dvd_of_dvd` (#15642)

feat(data/nat/totient): add lemma `totient_dvd_of_dvd` (#15642) Adds `totient_dvd_of_dvd (h : a ∣ b) : φ a ∣ φ b`. This is Theorem 2.5(d) in Apostol (1976) Introduction to Analytic Number Theory.