Multiplicativity of ideal Dirichlet convolution #
Dirichlet convolution preserves multiplicativity on relatively prime nonzero ideals. Factorizations of a relatively prime product are obtained uniquely by multiplying factorizations of its two factors. This supplies the multiplicativity needed to form products of ideal Euler products.
References #
- The factorization reindexing follows Mathlib’s
ArithmeticFunction.IsMultiplicative.mul, with divisor decomposition in the ideal monoid replacing the natural-number gcd argument. - G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.2.
theorem
TauCeti.IdealArithmeticFunction.IsMultiplicative.convolution
{K : Type u_1}
[Field K]
[NumberField K]
{f g : IdealArithmeticFunction K}
(hf : f.IsMultiplicative)
(hg : g.IsMultiplicative)
:
(f.convolution g).IsMultiplicative
Dirichlet convolution of two coprime-multiplicative ideal arithmetic functions is coprime-multiplicative.