Theorems · Definition · number theory

ArithmeticFunction

(R : Type u_1) → [Zero R] → Type (max 0 u_1)

An arithmetic function is a function from ℕ that maps 0 to 0. In the literature, they are often instead defined as functions from ℕ+. Multiplication on ArithmeticFunctions is by Dirichlet convolution.

Defined in

Mathlib.NumberTheory.ArithmeticFunction.Defs

Cited by

290 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 113 definitions · uses propext

Assumes

Zero