Arithmetic functions

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-03-23.
Last modified on 2023-03-13.

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

Recent changes