Commit 2022-05-13 15:42 6b7fa7ab

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.