mathlib3

565e961d - feat(number_theory/arithmetic_function): Define arithmetic functions/the Dirichlet ring (#4352)

feat(number_theory/arithmetic_function): Define arithmetic functions/the Dirichlet ring (#4352) Defines a type `arithmetic_function A` of functions from `nat` to `A` sending 0 to 0 Defines the Dirichlet ring structure on `arithmetic_function A` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>