Arithmetic functions

module elementary-number-theory.arithmetic-functions where
Imports
open import elementary-number-theory.nonzero-natural-numbers

open import foundation.universe-levels

open import ring-theory.rings

Idea

An arithmetic function is a function from the nonzero natural numbers into a (commutative) ring. The arithmetic functions form a ring under pointwise addition and dirichlet convolution.

Definition

module _
  {l : Level} (R : Ring l)
  where

  type-arithmetic-functions-Ring : UU l
  type-arithmetic-functions-Ring = nonzero-ℕ  type-Ring R