Commit 2023-12-27 17:24 49d59e74

View on Github →

feat: define prodPrimeFactors as an ArithmeticFunction (#6662) Define the arithmetic function $n \mapsto \prod_{p \mid n} f(p)$. This PR further proves that it's multiplicative and relates it to Dirichlet convolution. Finally it proves two identities that can be applied in a context where you're not working exclusively with ArithmeticFunctions This construction was mentioned on zulip

Estimated changes

Modified Mathlib/Data/Nat/Squarefree.lean

added theorem Nat.prod_primeFactors_sdiff_of_squarefree

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod_of_prime

added theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors

added theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors

added theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree

added theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree

added theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree

added def Nat.ArithmeticFunction.prodPrimeFactors

added theorem Nat.ArithmeticFunction.prodPrimeFactors_apply

added theorem Nat.ArithmeticFunction.prodPrimeFactors_apply_of_ne_zero