Completely multiplicative functions

DefinitionCompletely multiplicative arithmetic function#✓fully proved

Let \(R\) be a type with a multiplication and a zero. An arithmetic function \(f\) with values in \(R\) (so \(f(0) = 0\)) is completely multiplicative if \(f(mn) = f(m) f(n)\) for all \(m, n \in \mathbb{N} = \{0, 1, 2, \dots\}\).

The normalization \(f(1) = 1\) is not part of the definition.

def IsCompletelyMultiplicative [Mul R] [Zero R] (f : ArithmeticFunction R) : Prop :=
  ∀ m n : ℕ, f (m * n) = f m * f n

Used by 7

Used byNormalized completely multiplicative functions are multiplicative · Completely multiplicative functions preserve products · Complete multiplicativity of \(c^{\Omega}\) · Gcd expansion of a convolution of completely multiplicative functions at a product · Sums of a Dirichlet convolution over multiples of \(r\) · Weighted summation of Dirichlet convolutions · Bound for a Dirichlet series by its prime sum

TheoremCompletely multiplicative functions preserve products#✓fully proved

Let \(R\) be a type with a multiplication and a zero, and let \(f\) be a completely multiplicative arithmetic function with values in \(R\). Then \(f(mn) = f(m) f(n)\) for all \(m, n \in \mathbb{N}\).

@[simp]
theorem IsCompletelyMultiplicative.map_mul [Mul R] [Zero R] {f : ArithmeticFunction R}
    (hf : f.IsCompletelyMultiplicative) (m n : ℕ) : f (m * n) = f m * f n

Uses 1

Statement usesCompletely multiplicative arithmetic function

TheoremNormalized completely multiplicative functions are multiplicative#✓fully proved

Let \(R\) be a monoid with zero and let \(f\) be a completely multiplicative arithmetic function with values in \(R\) such that \(f(1) = 1\). Then \(f\) is multiplicative: \(f(1) = 1\) and \(f(mn) = f(m) f(n)\) for all coprime natural numbers \(m\) and \(n\).

theorem IsCompletelyMultiplicative.isMultiplicative [MonoidWithZero R]
    {f : ArithmeticFunction R} (hf : f.IsCompletelyMultiplicative) (h1 : f 1 = 1) :
    f.IsMultiplicative

Uses 1 · Used by 1

Statement usesCompletely multiplicative arithmetic function

Used byMultiplicativity of \(c^{\Omega}\)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.