noncomputable def mulConv (f g : ℕ → ℂ) (n : ℕ) : ℂ

The multiplicative (Dirichlet) convolution of two functions $f, g : \mathbb{N} \to \mathbb{C}$: $(f *_M g)(n) = \sum_{n_1 n_2 = n} f(n_1)\, g(n_2)$.

theorem MultiplicativeConvolution.mulConv_eq_arithmeticFunction_mul (f g : ArithmeticFunction ℂ) (n : ℕ) : mulConv (fun (n : ℕ) => f n) (fun (n : ℕ) => g n) n = (f * g) n

The multiplicative convolution mulConv agrees pointwise with the product f * g of arithmetic functions (i.e. with Dirichlet convolution defined on ArithmeticFunction ℂ).