Commit 2020-10-05 07:39 565e961d
View on Github →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