Commit 2025-12-02 09:01 4aacc267

View on Github →

refactor(NumberTheory/ArithmeticFunction): split long file (#32304) Split the > 1500 line Mathlib.NumberTheory.ArithmeticFunction into several smaller pieces.

Estimated changes

Modified Archive/Wiedijk100Theorems/PerfectNumbers.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

deleted theorem ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers

deleted theorem ArithmeticFunction.IsMultiplicative.eq_zero_of_squarefree_of_dvd_eq_zero

deleted theorem ArithmeticFunction.IsMultiplicative.iff_ne_zero

deleted theorem ArithmeticFunction.IsMultiplicative.intCast

deleted theorem ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply

deleted theorem ArithmeticFunction.IsMultiplicative.map_div_of_coprime

deleted theorem ArithmeticFunction.IsMultiplicative.map_gcd

deleted theorem ArithmeticFunction.IsMultiplicative.map_lcm

deleted theorem ArithmeticFunction.IsMultiplicative.map_mul_of_coprime

deleted theorem ArithmeticFunction.IsMultiplicative.map_one

deleted theorem ArithmeticFunction.IsMultiplicative.map_prod

deleted theorem ArithmeticFunction.IsMultiplicative.map_prod_of_prime

deleted theorem ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors

deleted theorem ArithmeticFunction.IsMultiplicative.mul

deleted theorem ArithmeticFunction.IsMultiplicative.multiplicative_factorization

deleted theorem ArithmeticFunction.IsMultiplicative.natCast

deleted theorem ArithmeticFunction.IsMultiplicative.pdiv

deleted theorem ArithmeticFunction.IsMultiplicative.pmul

deleted theorem ArithmeticFunction.IsMultiplicative.ppow

deleted theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors

deleted theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree

deleted theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree

deleted theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree

deleted theorem ArithmeticFunction.IsMultiplicative.prod_primeFactors

deleted def ArithmeticFunction.IsMultiplicative

deleted theorem ArithmeticFunction.abs_moebius

deleted theorem ArithmeticFunction.abs_moebius_eq_one_of_squarefree

deleted theorem ArithmeticFunction.abs_moebius_le_one

deleted theorem ArithmeticFunction.add_apply

deleted def ArithmeticFunction.cardDistinctFactors

deleted theorem ArithmeticFunction.cardDistinctFactors_apply

deleted theorem ArithmeticFunction.cardDistinctFactors_apply_prime

deleted theorem ArithmeticFunction.cardDistinctFactors_apply_prime_pow

deleted theorem ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree

deleted theorem ArithmeticFunction.cardDistinctFactors_eq_one_iff

deleted theorem ArithmeticFunction.cardDistinctFactors_eq_zero

deleted theorem ArithmeticFunction.cardDistinctFactors_mul

deleted theorem ArithmeticFunction.cardDistinctFactors_one

deleted theorem ArithmeticFunction.cardDistinctFactors_pos

deleted theorem ArithmeticFunction.cardDistinctFactors_prod

deleted theorem ArithmeticFunction.cardDistinctFactors_zero

deleted def ArithmeticFunction.cardFactors

deleted theorem ArithmeticFunction.cardFactors_apply

deleted theorem ArithmeticFunction.cardFactors_apply_prime

deleted theorem ArithmeticFunction.cardFactors_apply_prime_pow

deleted theorem ArithmeticFunction.cardFactors_eq_one_iff_prime

deleted theorem ArithmeticFunction.cardFactors_eq_sum_factorization

deleted theorem ArithmeticFunction.cardFactors_eq_zero_iff_eq_zero_or_one

deleted theorem ArithmeticFunction.cardFactors_mul

deleted theorem ArithmeticFunction.cardFactors_multiset_prod

deleted theorem ArithmeticFunction.cardFactors_one

deleted theorem ArithmeticFunction.cardFactors_pos_iff_one_lt

deleted theorem ArithmeticFunction.cardFactors_pow

deleted theorem ArithmeticFunction.cardFactors_zero

deleted theorem ArithmeticFunction.coe_coe

deleted theorem ArithmeticFunction.coe_inj

deleted theorem ArithmeticFunction.coe_mk

deleted theorem ArithmeticFunction.coe_moebius_mul_coe_zeta

deleted theorem ArithmeticFunction.coe_mul_zeta_apply

deleted theorem ArithmeticFunction.coe_zetaUnit

deleted theorem ArithmeticFunction.coe_zeta_mul_apply

deleted theorem ArithmeticFunction.coe_zeta_mul_coe_moebius

deleted theorem ArithmeticFunction.coe_zeta_mul_comm

deleted theorem ArithmeticFunction.coe_zeta_mul_moebius

deleted theorem ArithmeticFunction.coe_zeta_smul_apply

deleted theorem ArithmeticFunction.ext

deleted def ArithmeticFunction.id

deleted theorem ArithmeticFunction.id_apply

deleted theorem ArithmeticFunction.intCoe_apply

deleted theorem ArithmeticFunction.intCoe_int

deleted theorem ArithmeticFunction.intCoe_mul

deleted theorem ArithmeticFunction.intCoe_one

deleted theorem ArithmeticFunction.inv_zetaUnit

deleted theorem ArithmeticFunction.isMultiplicative_id

deleted theorem ArithmeticFunction.isMultiplicative_moebius

deleted theorem ArithmeticFunction.isMultiplicative_one

deleted theorem ArithmeticFunction.isMultiplicative_pow

deleted theorem ArithmeticFunction.isMultiplicative_sigma

deleted theorem ArithmeticFunction.isMultiplicative_zeta

deleted theorem ArithmeticFunction.map_zero

deleted def ArithmeticFunction.moebius

deleted theorem ArithmeticFunction.moebius_apply_isPrimePow_not_prime

deleted theorem ArithmeticFunction.moebius_apply_of_squarefree

deleted theorem ArithmeticFunction.moebius_apply_one

deleted theorem ArithmeticFunction.moebius_apply_prime

deleted theorem ArithmeticFunction.moebius_apply_prime_pow

deleted theorem ArithmeticFunction.moebius_eq_or

deleted theorem ArithmeticFunction.moebius_eq_zero_of_not_squarefree

deleted theorem ArithmeticFunction.moebius_mul_coe_zeta

deleted theorem ArithmeticFunction.moebius_ne_zero_iff_eq_or

deleted theorem ArithmeticFunction.moebius_ne_zero_iff_squarefree

deleted theorem ArithmeticFunction.moebius_sq

deleted theorem ArithmeticFunction.moebius_sq_eq_one_of_squarefree

deleted theorem ArithmeticFunction.mul_apply

deleted theorem ArithmeticFunction.mul_apply_one

deleted theorem ArithmeticFunction.mul_smul'

deleted theorem ArithmeticFunction.mul_zeta_apply

deleted theorem ArithmeticFunction.natCoe_apply

deleted theorem ArithmeticFunction.natCoe_mul

deleted theorem ArithmeticFunction.natCoe_nat

deleted theorem ArithmeticFunction.natCoe_one

deleted def ArithmeticFunction.natToArithmeticFunction

deleted def ArithmeticFunction.ofInt

deleted theorem ArithmeticFunction.one_apply

deleted theorem ArithmeticFunction.one_apply_ne

deleted theorem ArithmeticFunction.one_one

deleted theorem ArithmeticFunction.one_smul'

deleted def ArithmeticFunction.pdiv

deleted theorem ArithmeticFunction.pdiv_apply

deleted theorem ArithmeticFunction.pdiv_zeta

deleted def ArithmeticFunction.pmul

deleted theorem ArithmeticFunction.pmul_apply

deleted theorem ArithmeticFunction.pmul_assoc

deleted theorem ArithmeticFunction.pmul_comm

deleted theorem ArithmeticFunction.pmul_zeta

deleted def ArithmeticFunction.pow

deleted theorem ArithmeticFunction.pow_apply

deleted theorem ArithmeticFunction.pow_one_eq_id

deleted theorem ArithmeticFunction.pow_zero_eq_zeta

deleted def ArithmeticFunction.ppow

deleted theorem ArithmeticFunction.ppow_apply

deleted theorem ArithmeticFunction.ppow_one

deleted theorem ArithmeticFunction.ppow_succ'

deleted theorem ArithmeticFunction.ppow_succ

deleted theorem ArithmeticFunction.ppow_zero

deleted def ArithmeticFunction.prodPrimeFactors

deleted theorem ArithmeticFunction.prodPrimeFactors_apply

deleted theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq

deleted theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero

deleted theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on

deleted theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero

deleted def ArithmeticFunction.sigma

deleted theorem ArithmeticFunction.sigma_apply

deleted theorem ArithmeticFunction.sigma_apply_prime_pow

deleted theorem ArithmeticFunction.sigma_eq_one_iff

deleted theorem ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul

deleted theorem ArithmeticFunction.sigma_eq_sum_div

deleted theorem ArithmeticFunction.sigma_eq_zero

deleted theorem ArithmeticFunction.sigma_mono

deleted theorem ArithmeticFunction.sigma_one

deleted theorem ArithmeticFunction.sigma_one_apply

deleted theorem ArithmeticFunction.sigma_one_apply_prime_pow

deleted theorem ArithmeticFunction.sigma_pos

deleted theorem ArithmeticFunction.sigma_pos_iff

deleted theorem ArithmeticFunction.sigma_zero_apply

deleted theorem ArithmeticFunction.sigma_zero_apply_prime_pow

deleted theorem ArithmeticFunction.smul_apply

deleted theorem ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter

deleted theorem ArithmeticFunction.sum_Ioc_mul_eq_sum_sum

deleted theorem ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum

deleted theorem ArithmeticFunction.sum_Ioc_sigma0_eq_sum_div

deleted theorem ArithmeticFunction.sum_Ioc_zeta

deleted theorem ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors

deleted theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq

deleted theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on

deleted theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq

deleted theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on'

deleted theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on

deleted theorem ArithmeticFunction.toFun_eq

deleted theorem ArithmeticFunction.zero_apply

deleted def ArithmeticFunction.zeta

deleted def ArithmeticFunction.zetaUnit

deleted theorem ArithmeticFunction.zeta_apply

deleted theorem ArithmeticFunction.zeta_apply_ne

deleted theorem ArithmeticFunction.zeta_eq_zero

deleted theorem ArithmeticFunction.zeta_mul_apply

deleted theorem ArithmeticFunction.zeta_mul_comm

deleted theorem ArithmeticFunction.zeta_mul_pow_eq_sigma

deleted theorem ArithmeticFunction.zeta_pmul

deleted theorem ArithmeticFunction.zeta_pos

deleted def ArithmeticFunction

deleted theorem Nat.Coprime.card_divisors_mul

deleted theorem Nat.Coprime.sum_divisors_mul

deleted theorem Nat.card_divisors

deleted theorem Nat.divisors_card_eq_one_iff

deleted theorem Nat.sum_divisors

Created Mathlib/NumberTheory/ArithmeticFunction/Defs.lean

added theorem ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers

added theorem ArithmeticFunction.IsMultiplicative.eq_zero_of_squarefree_of_dvd_eq_zero

added theorem ArithmeticFunction.IsMultiplicative.iff_ne_zero

added theorem ArithmeticFunction.IsMultiplicative.intCast

added theorem ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply

added theorem ArithmeticFunction.IsMultiplicative.map_div_of_coprime

added theorem ArithmeticFunction.IsMultiplicative.map_gcd

added theorem ArithmeticFunction.IsMultiplicative.map_lcm

added theorem ArithmeticFunction.IsMultiplicative.map_mul_of_coprime

added theorem ArithmeticFunction.IsMultiplicative.map_one

added theorem ArithmeticFunction.IsMultiplicative.map_prod

added theorem ArithmeticFunction.IsMultiplicative.map_prod_of_prime

added theorem ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors

added theorem ArithmeticFunction.IsMultiplicative.mul

added theorem ArithmeticFunction.IsMultiplicative.multiplicative_factorization

added theorem ArithmeticFunction.IsMultiplicative.natCast

added theorem ArithmeticFunction.IsMultiplicative.prod_primeFactors

added def ArithmeticFunction.IsMultiplicative

added theorem ArithmeticFunction.add_apply

added theorem ArithmeticFunction.coe_coe

added theorem ArithmeticFunction.coe_inj

added theorem ArithmeticFunction.coe_mk

added theorem ArithmeticFunction.ext

added theorem ArithmeticFunction.intCoe_apply

added theorem ArithmeticFunction.intCoe_int

added theorem ArithmeticFunction.intCoe_mul

added theorem ArithmeticFunction.intCoe_one

added theorem ArithmeticFunction.isMultiplicative_one

added theorem ArithmeticFunction.map_zero

added theorem ArithmeticFunction.mul_apply

added theorem ArithmeticFunction.mul_apply_one

added theorem ArithmeticFunction.mul_smul'

added theorem ArithmeticFunction.natCoe_apply

added theorem ArithmeticFunction.natCoe_mul

added theorem ArithmeticFunction.natCoe_nat

added theorem ArithmeticFunction.natCoe_one

added def ArithmeticFunction.natToArithmeticFunction

added def ArithmeticFunction.ofInt

added theorem ArithmeticFunction.one_apply

added theorem ArithmeticFunction.one_apply_ne

added theorem ArithmeticFunction.one_one

added theorem ArithmeticFunction.one_smul'

added theorem ArithmeticFunction.smul_apply

added theorem ArithmeticFunction.toFun_eq

added theorem ArithmeticFunction.zero_apply

added def ArithmeticFunction

Created Mathlib/NumberTheory/ArithmeticFunction/Misc.lean

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree

added def ArithmeticFunction.cardDistinctFactors

added theorem ArithmeticFunction.cardDistinctFactors_apply

added theorem ArithmeticFunction.cardDistinctFactors_apply_prime

added theorem ArithmeticFunction.cardDistinctFactors_apply_prime_pow

added theorem ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree

added theorem ArithmeticFunction.cardDistinctFactors_eq_one_iff

added theorem ArithmeticFunction.cardDistinctFactors_eq_zero

added theorem ArithmeticFunction.cardDistinctFactors_mul

added theorem ArithmeticFunction.cardDistinctFactors_one

added theorem ArithmeticFunction.cardDistinctFactors_pos

added theorem ArithmeticFunction.cardDistinctFactors_prod

added theorem ArithmeticFunction.cardDistinctFactors_zero

added def ArithmeticFunction.cardFactors

added theorem ArithmeticFunction.cardFactors_apply

added theorem ArithmeticFunction.cardFactors_apply_prime

added theorem ArithmeticFunction.cardFactors_apply_prime_pow

added theorem ArithmeticFunction.cardFactors_eq_one_iff_prime

added theorem ArithmeticFunction.cardFactors_eq_sum_factorization

added theorem ArithmeticFunction.cardFactors_eq_zero_iff_eq_zero_or_one

added theorem ArithmeticFunction.cardFactors_mul

added theorem ArithmeticFunction.cardFactors_multiset_prod

added theorem ArithmeticFunction.cardFactors_one

added theorem ArithmeticFunction.cardFactors_pos_iff_one_lt

added theorem ArithmeticFunction.cardFactors_pow

added theorem ArithmeticFunction.cardFactors_zero

added def ArithmeticFunction.id

added theorem ArithmeticFunction.id_apply

added theorem ArithmeticFunction.isMultiplicative_id

added theorem ArithmeticFunction.isMultiplicative_pow

added theorem ArithmeticFunction.isMultiplicative_sigma

added def ArithmeticFunction.pow

added theorem ArithmeticFunction.pow_apply

added theorem ArithmeticFunction.pow_one_eq_id

added theorem ArithmeticFunction.pow_zero_eq_zeta

added def ArithmeticFunction.prodPrimeFactors

added theorem ArithmeticFunction.prodPrimeFactors_apply

added def ArithmeticFunction.sigma

added theorem ArithmeticFunction.sigma_apply

added theorem ArithmeticFunction.sigma_apply_prime_pow

added theorem ArithmeticFunction.sigma_eq_one_iff

added theorem ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul

added theorem ArithmeticFunction.sigma_eq_sum_div

added theorem ArithmeticFunction.sigma_eq_zero

added theorem ArithmeticFunction.sigma_mono

added theorem ArithmeticFunction.sigma_one

added theorem ArithmeticFunction.sigma_one_apply

added theorem ArithmeticFunction.sigma_one_apply_prime_pow

added theorem ArithmeticFunction.sigma_pos

added theorem ArithmeticFunction.sigma_pos_iff

added theorem ArithmeticFunction.sigma_zero_apply

added theorem ArithmeticFunction.sigma_zero_apply_prime_pow

added theorem ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter

added theorem ArithmeticFunction.sum_Ioc_mul_eq_sum_sum

added theorem ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum

added theorem ArithmeticFunction.sum_Ioc_sigma0_eq_sum_div

added theorem ArithmeticFunction.sum_Ioc_zeta

added theorem ArithmeticFunction.zeta_mul_pow_eq_sigma

added theorem Nat.Coprime.card_divisors_mul

added theorem Nat.Coprime.sum_divisors_mul

added theorem Nat.card_divisors

added theorem Nat.divisors_card_eq_one_iff

added theorem Nat.sum_divisors

Created Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree

added theorem ArithmeticFunction.abs_moebius

added theorem ArithmeticFunction.abs_moebius_eq_one_of_squarefree

added theorem ArithmeticFunction.abs_moebius_le_one

added theorem ArithmeticFunction.coe_moebius_mul_coe_zeta

added theorem ArithmeticFunction.coe_zetaUnit

added theorem ArithmeticFunction.coe_zeta_mul_coe_moebius

added theorem ArithmeticFunction.coe_zeta_mul_moebius

added theorem ArithmeticFunction.inv_zetaUnit

added theorem ArithmeticFunction.isMultiplicative_moebius

added def ArithmeticFunction.moebius

added theorem ArithmeticFunction.moebius_apply_isPrimePow_not_prime

added theorem ArithmeticFunction.moebius_apply_of_squarefree

added theorem ArithmeticFunction.moebius_apply_one

added theorem ArithmeticFunction.moebius_apply_prime

added theorem ArithmeticFunction.moebius_apply_prime_pow

added theorem ArithmeticFunction.moebius_eq_or

added theorem ArithmeticFunction.moebius_eq_zero_of_not_squarefree

added theorem ArithmeticFunction.moebius_mul_coe_zeta

added theorem ArithmeticFunction.moebius_ne_zero_iff_eq_or

added theorem ArithmeticFunction.moebius_ne_zero_iff_squarefree

added theorem ArithmeticFunction.moebius_sq

added theorem ArithmeticFunction.moebius_sq_eq_one_of_squarefree

added theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq

added theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero

added theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on

added theorem ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero

added theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq

added theorem ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on

added theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq

added theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on'

added theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on

added def ArithmeticFunction.zetaUnit

Created Mathlib/NumberTheory/ArithmeticFunction/VonMangoldt.lean

added theorem ArithmeticFunction.log_apply

added theorem ArithmeticFunction.log_mul_moebius_eq_vonMangoldt

added theorem ArithmeticFunction.moebius_mul_log_eq_vonMangoldt

added theorem ArithmeticFunction.sum_moebius_mul_log_eq

added theorem ArithmeticFunction.vonMangoldt_apply

added theorem ArithmeticFunction.vonMangoldt_apply_one

added theorem ArithmeticFunction.vonMangoldt_apply_pow

added theorem ArithmeticFunction.vonMangoldt_apply_prime

added theorem ArithmeticFunction.vonMangoldt_eq_zero_iff

added theorem ArithmeticFunction.vonMangoldt_le_log

added theorem ArithmeticFunction.vonMangoldt_mul_zeta

added theorem ArithmeticFunction.vonMangoldt_ne_zero_iff

added theorem ArithmeticFunction.vonMangoldt_nonneg

added theorem ArithmeticFunction.vonMangoldt_pos_iff

added theorem ArithmeticFunction.vonMangoldt_sum

added theorem ArithmeticFunction.zeta_mul_vonMangoldt

Created Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean

added theorem ArithmeticFunction.IsMultiplicative.pdiv

added theorem ArithmeticFunction.IsMultiplicative.pmul

added theorem ArithmeticFunction.IsMultiplicative.ppow

added theorem ArithmeticFunction.coe_mul_zeta_apply

added theorem ArithmeticFunction.coe_zeta_mul_apply

added theorem ArithmeticFunction.coe_zeta_mul_comm

added theorem ArithmeticFunction.coe_zeta_smul_apply

added theorem ArithmeticFunction.isMultiplicative_zeta

added theorem ArithmeticFunction.mul_zeta_apply

added def ArithmeticFunction.pdiv

added theorem ArithmeticFunction.pdiv_apply

added theorem ArithmeticFunction.pdiv_zeta

added def ArithmeticFunction.pmul

added theorem ArithmeticFunction.pmul_apply

added theorem ArithmeticFunction.pmul_assoc

added theorem ArithmeticFunction.pmul_comm

added theorem ArithmeticFunction.pmul_zeta

added def ArithmeticFunction.ppow

added theorem ArithmeticFunction.ppow_apply

added theorem ArithmeticFunction.ppow_one

added theorem ArithmeticFunction.ppow_succ'

added theorem ArithmeticFunction.ppow_succ

added theorem ArithmeticFunction.ppow_zero

added theorem ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors

added def ArithmeticFunction.zeta

added theorem ArithmeticFunction.zeta_apply

added theorem ArithmeticFunction.zeta_apply_ne

added theorem ArithmeticFunction.zeta_eq_zero

added theorem ArithmeticFunction.zeta_mul_apply

added theorem ArithmeticFunction.zeta_mul_comm

added theorem ArithmeticFunction.zeta_pmul

added theorem ArithmeticFunction.zeta_pos

Modified Mathlib/NumberTheory/EulerProduct/Basic.lean

Modified Mathlib/NumberTheory/LSeries/Convolution.lean

Modified Mathlib/NumberTheory/LSeries/Dirichlet.lean

Modified Mathlib/NumberTheory/LSeries/Positivity.lean

Modified Mathlib/NumberTheory/SelbergSieve.lean

Modified Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

Modified Mathlib/NumberTheory/VonMangoldt.lean

deleted theorem ArithmeticFunction.log_apply

deleted theorem ArithmeticFunction.log_mul_moebius_eq_vonMangoldt

deleted theorem ArithmeticFunction.moebius_mul_log_eq_vonMangoldt

deleted theorem ArithmeticFunction.sum_moebius_mul_log_eq

deleted theorem ArithmeticFunction.vonMangoldt_apply

deleted theorem ArithmeticFunction.vonMangoldt_apply_one

deleted theorem ArithmeticFunction.vonMangoldt_apply_pow

deleted theorem ArithmeticFunction.vonMangoldt_apply_prime

deleted theorem ArithmeticFunction.vonMangoldt_eq_zero_iff

deleted theorem ArithmeticFunction.vonMangoldt_le_log

deleted theorem ArithmeticFunction.vonMangoldt_mul_zeta

deleted theorem ArithmeticFunction.vonMangoldt_ne_zero_iff

deleted theorem ArithmeticFunction.vonMangoldt_nonneg

deleted theorem ArithmeticFunction.vonMangoldt_pos_iff

deleted theorem ArithmeticFunction.vonMangoldt_sum

deleted theorem ArithmeticFunction.zeta_mul_vonMangoldt

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified MathlibTest/ArithMult.lean

Modified MathlibTest/positivity.lean