mathlib3

f4c67ee5 - chore(group_theory/specific_groups/cyclic): golf `card_order_of_eq_totient_aux₁` and `card_order_of_eq_totient_aux₂` (#14161)

chore(group_theory/specific_groups/cyclic): golf `card_order_of_eq_totient_aux₁` and `card_order_of_eq_totient_aux₂` (#14161) Re-writing the proofs of `card_order_of_eq_totient_aux₁` and `card_order_of_eq_totient_aux₂` to use the new `sum_totient` introduced in #14007, and golfing them.