Commit 2022-08-10 08:06 7c205ffb
View on Github →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.
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.