mathlib

947d5f47 - Eliminate `finish` from `sum_totient`