mathlib3

6b7fa7ab - feat(data/nat/totient): add `totient_div_of_dvd` and golf `sum_totient` (#14007)

feat(data/nat/totient): add `totient_div_of_dvd` and golf `sum_totient` (#14007) Add lemma `totient_div_of_dvd`: for `d ∣ n`, the totient of `n/d` equals the number of values `k < n` such that `gcd n k = d`. Use this to golf `sum_totient`, now stated in terms of `divisors`. This proof follows that of Theorem 2.2 in Apostol (1976) Introduction to Analytic Number Theory. Adapt the proof of `nth_roots_one_eq_bUnion_primitive_roots'` to use the new `sum_totient`. Re-prove the original statement of `sum_totient` for compatibility with uses in `group_theory/specific_groups/cyclic` — may delete this if those uses can be adapted to the new statement.