Commit 2024-02-10 13:10 a6a17daf

View on Github →

chore(NumberTheory/ArithmeticFunction): remove Nat. part from ArithmeticFunction namespace (#10399) This changes Nat.ArithmeticFunction to ArithmeticFunction since the Nat part seems redundant. See here on Zulip.

Estimated changes

Modified Archive/Wiedijk100Theorems/PerfectNumbers.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers

added theorem ArithmeticFunction.IsMultiplicative.iff_ne_zero

added theorem ArithmeticFunction.IsMultiplicative.int_cast

added theorem ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply

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.nat_cast

added theorem ArithmeticFunction.IsMultiplicative.pdiv

added theorem ArithmeticFunction.IsMultiplicative.pmul

added theorem ArithmeticFunction.IsMultiplicative.ppow

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree

added theorem ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree

added def ArithmeticFunction.IsMultiplicative

added theorem ArithmeticFunction.add_apply

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_one

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_mul

added theorem ArithmeticFunction.cardFactors_multiset_prod

added theorem ArithmeticFunction.cardFactors_one

added theorem ArithmeticFunction.cardFactors_zero

added theorem ArithmeticFunction.coe_coe

added theorem ArithmeticFunction.coe_inj

added theorem ArithmeticFunction.coe_mk

added theorem ArithmeticFunction.coe_moebius_mul_coe_zeta

added theorem ArithmeticFunction.coe_mul_zeta_apply

added theorem ArithmeticFunction.coe_zetaUnit

added theorem ArithmeticFunction.coe_zeta_mul_apply

added theorem ArithmeticFunction.coe_zeta_mul_coe_moebius

added theorem ArithmeticFunction.coe_zeta_mul_moebius

added theorem ArithmeticFunction.coe_zeta_smul_apply

added theorem ArithmeticFunction.ext

added theorem ArithmeticFunction.ext_iff

added def ArithmeticFunction.id

added theorem ArithmeticFunction.id_apply

added theorem ArithmeticFunction.intCoe_apply

added theorem ArithmeticFunction.intCoe_int

added theorem ArithmeticFunction.intCoe_mul

added theorem ArithmeticFunction.intCoe_one

added theorem ArithmeticFunction.inv_zetaUnit

added theorem ArithmeticFunction.isMultiplicative_id

added theorem ArithmeticFunction.isMultiplicative_moebius

added theorem ArithmeticFunction.isMultiplicative_one

added theorem ArithmeticFunction.isMultiplicative_pow

added theorem ArithmeticFunction.isMultiplicative_sigma

added theorem ArithmeticFunction.isMultiplicative_zeta

added theorem ArithmeticFunction.map_zero

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_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.mul_apply

added theorem ArithmeticFunction.mul_apply_one

added theorem ArithmeticFunction.mul_smul'

added theorem ArithmeticFunction.mul_zeta_apply

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 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_comm

added theorem ArithmeticFunction.pmul_zeta

added def ArithmeticFunction.pow

added theorem ArithmeticFunction.pow_apply

added theorem ArithmeticFunction.pow_zero_eq_zeta

added def ArithmeticFunction.ppow

added theorem ArithmeticFunction.ppow_apply

added theorem ArithmeticFunction.ppow_succ'

added theorem ArithmeticFunction.ppow_succ

added theorem ArithmeticFunction.ppow_zero

added def ArithmeticFunction.prodPrimeFactors

added theorem ArithmeticFunction.prodPrimeFactors_apply

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 def ArithmeticFunction.sigma

added theorem ArithmeticFunction.sigma_apply

added theorem ArithmeticFunction.sigma_one_apply

added theorem ArithmeticFunction.sigma_zero_apply

added theorem ArithmeticFunction.sigma_zero_apply_prime_pow

added theorem ArithmeticFunction.smul_apply

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 theorem ArithmeticFunction.toFun_eq

added theorem ArithmeticFunction.zero_apply

added def ArithmeticFunction.zeta

added def ArithmeticFunction.zetaUnit

added theorem ArithmeticFunction.zeta_apply

added theorem ArithmeticFunction.zeta_apply_ne

added theorem ArithmeticFunction.zeta_mul_apply

added theorem ArithmeticFunction.zeta_mul_pow_eq_sigma

added theorem ArithmeticFunction.zeta_pmul

added def ArithmeticFunction

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.iff_ne_zero

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.int_cast

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.map_mul_of_coprime

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.map_one

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod_of_prime

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.mul

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.multiplicative_factorization

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.nat_cast

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.pdiv

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.pmul

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.ppow

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_add_of_squarefree

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree

deleted theorem Nat.ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree

deleted def Nat.ArithmeticFunction.IsMultiplicative

deleted theorem Nat.ArithmeticFunction.add_apply

deleted def Nat.ArithmeticFunction.cardDistinctFactors

deleted theorem Nat.ArithmeticFunction.cardDistinctFactors_apply

deleted theorem Nat.ArithmeticFunction.cardDistinctFactors_apply_prime

deleted theorem Nat.ArithmeticFunction.cardDistinctFactors_apply_prime_pow

deleted theorem Nat.ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree

deleted theorem Nat.ArithmeticFunction.cardDistinctFactors_one

deleted theorem Nat.ArithmeticFunction.cardDistinctFactors_zero

deleted def Nat.ArithmeticFunction.cardFactors

deleted theorem Nat.ArithmeticFunction.cardFactors_apply

deleted theorem Nat.ArithmeticFunction.cardFactors_apply_prime

deleted theorem Nat.ArithmeticFunction.cardFactors_apply_prime_pow

deleted theorem Nat.ArithmeticFunction.cardFactors_eq_one_iff_prime

deleted theorem Nat.ArithmeticFunction.cardFactors_mul

deleted theorem Nat.ArithmeticFunction.cardFactors_multiset_prod

deleted theorem Nat.ArithmeticFunction.cardFactors_one

deleted theorem Nat.ArithmeticFunction.cardFactors_zero

deleted theorem Nat.ArithmeticFunction.coe_coe

deleted theorem Nat.ArithmeticFunction.coe_inj

deleted theorem Nat.ArithmeticFunction.coe_mk

deleted theorem Nat.ArithmeticFunction.coe_moebius_mul_coe_zeta

deleted theorem Nat.ArithmeticFunction.coe_mul_zeta_apply

deleted theorem Nat.ArithmeticFunction.coe_zetaUnit

deleted theorem Nat.ArithmeticFunction.coe_zeta_mul_apply

deleted theorem Nat.ArithmeticFunction.coe_zeta_mul_coe_moebius

deleted theorem Nat.ArithmeticFunction.coe_zeta_mul_moebius

deleted theorem Nat.ArithmeticFunction.coe_zeta_smul_apply

deleted theorem Nat.ArithmeticFunction.ext

deleted theorem Nat.ArithmeticFunction.ext_iff

deleted def Nat.ArithmeticFunction.id

deleted theorem Nat.ArithmeticFunction.id_apply

deleted theorem Nat.ArithmeticFunction.intCoe_apply

deleted theorem Nat.ArithmeticFunction.intCoe_int

deleted theorem Nat.ArithmeticFunction.intCoe_mul

deleted theorem Nat.ArithmeticFunction.intCoe_one

deleted theorem Nat.ArithmeticFunction.inv_zetaUnit

deleted theorem Nat.ArithmeticFunction.isMultiplicative_id

deleted theorem Nat.ArithmeticFunction.isMultiplicative_moebius

deleted theorem Nat.ArithmeticFunction.isMultiplicative_one

deleted theorem Nat.ArithmeticFunction.isMultiplicative_pow

deleted theorem Nat.ArithmeticFunction.isMultiplicative_sigma

deleted theorem Nat.ArithmeticFunction.isMultiplicative_zeta

deleted theorem Nat.ArithmeticFunction.map_zero

deleted def Nat.ArithmeticFunction.moebius

deleted theorem Nat.ArithmeticFunction.moebius_apply_isPrimePow_not_prime

deleted theorem Nat.ArithmeticFunction.moebius_apply_of_squarefree

deleted theorem Nat.ArithmeticFunction.moebius_apply_one

deleted theorem Nat.ArithmeticFunction.moebius_apply_prime

deleted theorem Nat.ArithmeticFunction.moebius_apply_prime_pow

deleted theorem Nat.ArithmeticFunction.moebius_eq_zero_of_not_squarefree

deleted theorem Nat.ArithmeticFunction.moebius_mul_coe_zeta

deleted theorem Nat.ArithmeticFunction.moebius_ne_zero_iff_eq_or

deleted theorem Nat.ArithmeticFunction.moebius_ne_zero_iff_squarefree

deleted theorem Nat.ArithmeticFunction.mul_apply

deleted theorem Nat.ArithmeticFunction.mul_apply_one

deleted theorem Nat.ArithmeticFunction.mul_smul'

deleted theorem Nat.ArithmeticFunction.mul_zeta_apply

deleted theorem Nat.ArithmeticFunction.natCoe_apply

deleted theorem Nat.ArithmeticFunction.natCoe_mul

deleted theorem Nat.ArithmeticFunction.natCoe_nat

deleted theorem Nat.ArithmeticFunction.natCoe_one

deleted def Nat.ArithmeticFunction.natToArithmeticFunction

deleted def Nat.ArithmeticFunction.ofInt

deleted theorem Nat.ArithmeticFunction.one_apply

deleted theorem Nat.ArithmeticFunction.one_apply_ne

deleted theorem Nat.ArithmeticFunction.one_one

deleted theorem Nat.ArithmeticFunction.one_smul'

deleted def Nat.ArithmeticFunction.pdiv

deleted theorem Nat.ArithmeticFunction.pdiv_apply

deleted theorem Nat.ArithmeticFunction.pdiv_zeta

deleted def Nat.ArithmeticFunction.pmul

deleted theorem Nat.ArithmeticFunction.pmul_apply

deleted theorem Nat.ArithmeticFunction.pmul_comm

deleted theorem Nat.ArithmeticFunction.pmul_zeta

deleted def Nat.ArithmeticFunction.pow

deleted theorem Nat.ArithmeticFunction.pow_apply

deleted theorem Nat.ArithmeticFunction.pow_zero_eq_zeta

deleted def Nat.ArithmeticFunction.ppow

deleted theorem Nat.ArithmeticFunction.ppow_apply

deleted theorem Nat.ArithmeticFunction.ppow_succ'

deleted theorem Nat.ArithmeticFunction.ppow_succ

deleted theorem Nat.ArithmeticFunction.ppow_zero

deleted def Nat.ArithmeticFunction.prodPrimeFactors

deleted theorem Nat.ArithmeticFunction.prodPrimeFactors_apply

deleted theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq

deleted theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero

deleted theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on

deleted theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero

deleted def Nat.ArithmeticFunction.sigma

deleted theorem Nat.ArithmeticFunction.sigma_apply

deleted theorem Nat.ArithmeticFunction.sigma_one_apply

deleted theorem Nat.ArithmeticFunction.sigma_zero_apply

deleted theorem Nat.ArithmeticFunction.sigma_zero_apply_prime_pow

deleted theorem Nat.ArithmeticFunction.smul_apply

deleted theorem Nat.ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq

deleted theorem Nat.ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on

deleted theorem Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq

deleted theorem Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on'

deleted theorem Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on

deleted theorem Nat.ArithmeticFunction.toFun_eq

deleted theorem Nat.ArithmeticFunction.zero_apply

deleted def Nat.ArithmeticFunction.zeta

deleted def Nat.ArithmeticFunction.zetaUnit

deleted theorem Nat.ArithmeticFunction.zeta_apply

deleted theorem Nat.ArithmeticFunction.zeta_apply_ne

deleted theorem Nat.ArithmeticFunction.zeta_mul_apply

deleted theorem Nat.ArithmeticFunction.zeta_mul_pow_eq_sigma

deleted theorem Nat.ArithmeticFunction.zeta_pmul

deleted def Nat.ArithmeticFunction

Modified Mathlib/NumberTheory/EulerProduct/Basic.lean

Modified Mathlib/NumberTheory/LSeries/Basic.lean

added def ArithmeticFunction.LSeries

added def ArithmeticFunction.LSeriesSummable

added theorem ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re

added theorem ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re

added theorem ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real

added theorem ArithmeticFunction.LSeriesSummable_zero

added theorem ArithmeticFunction.LSeries_add

added theorem ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable

added theorem ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re

deleted def Nat.ArithmeticFunction.LSeries

deleted def Nat.ArithmeticFunction.LSeriesSummable

deleted theorem Nat.ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re

deleted theorem Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re

deleted theorem Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real

deleted theorem Nat.ArithmeticFunction.LSeriesSummable_zero

deleted theorem Nat.ArithmeticFunction.LSeries_add

deleted theorem Nat.ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable

deleted theorem Nat.ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re

Modified Mathlib/NumberTheory/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

deleted theorem Nat.ArithmeticFunction.log_apply

deleted theorem Nat.ArithmeticFunction.log_mul_moebius_eq_vonMangoldt

deleted theorem Nat.ArithmeticFunction.moebius_mul_log_eq_vonMangoldt

deleted theorem Nat.ArithmeticFunction.sum_moebius_mul_log_eq

deleted theorem Nat.ArithmeticFunction.vonMangoldt_apply

deleted theorem Nat.ArithmeticFunction.vonMangoldt_apply_one

deleted theorem Nat.ArithmeticFunction.vonMangoldt_apply_pow

deleted theorem Nat.ArithmeticFunction.vonMangoldt_apply_prime

deleted theorem Nat.ArithmeticFunction.vonMangoldt_eq_zero_iff

deleted theorem Nat.ArithmeticFunction.vonMangoldt_le_log

deleted theorem Nat.ArithmeticFunction.vonMangoldt_mul_zeta

deleted theorem Nat.ArithmeticFunction.vonMangoldt_ne_zero_iff

deleted theorem Nat.ArithmeticFunction.vonMangoldt_nonneg

deleted theorem Nat.ArithmeticFunction.vonMangoldt_pos_iff

deleted theorem Nat.ArithmeticFunction.vonMangoldt_sum

deleted theorem Nat.ArithmeticFunction.zeta_mul_vonMangoldt

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

Modified docs/overview.yaml