mathlib3

7368d719 - chore(number_theory/arithmetic_function): Define in terms of zero_hom (#4606)