Commit 2023-05-30 06:41 5c0483b6

View on Github →

feat: port NumberTheory.ArithmeticFunction (#4358)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem Nat.ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers

added theorem Nat.ArithmeticFunction.IsMultiplicative.iff_ne_zero

added theorem Nat.ArithmeticFunction.IsMultiplicative.int_cast

added theorem Nat.ArithmeticFunction.IsMultiplicative.map_mul_of_coprime

added theorem Nat.ArithmeticFunction.IsMultiplicative.map_one

added theorem Nat.ArithmeticFunction.IsMultiplicative.map_prod

added theorem Nat.ArithmeticFunction.IsMultiplicative.mul

added theorem Nat.ArithmeticFunction.IsMultiplicative.multiplicative_factorization

added theorem Nat.ArithmeticFunction.IsMultiplicative.nat_cast

added theorem Nat.ArithmeticFunction.IsMultiplicative.pmul

added theorem Nat.ArithmeticFunction.IsMultiplicative.ppow

added def Nat.ArithmeticFunction.IsMultiplicative

added theorem Nat.ArithmeticFunction.add_apply

added def Nat.ArithmeticFunction.cardDistinctFactors

added theorem Nat.ArithmeticFunction.cardDistinctFactors_apply

added theorem Nat.ArithmeticFunction.cardDistinctFactors_apply_prime

added theorem Nat.ArithmeticFunction.cardDistinctFactors_apply_prime_pow

added theorem Nat.ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree

added theorem Nat.ArithmeticFunction.cardDistinctFactors_one

added theorem Nat.ArithmeticFunction.cardDistinctFactors_zero

added def Nat.ArithmeticFunction.cardFactors

added theorem Nat.ArithmeticFunction.cardFactors_apply

added theorem Nat.ArithmeticFunction.cardFactors_apply_prime

added theorem Nat.ArithmeticFunction.cardFactors_apply_prime_pow

added theorem Nat.ArithmeticFunction.cardFactors_eq_one_iff_prime

added theorem Nat.ArithmeticFunction.cardFactors_mul

added theorem Nat.ArithmeticFunction.cardFactors_multiset_prod

added theorem Nat.ArithmeticFunction.cardFactors_one

added theorem Nat.ArithmeticFunction.coe_coe

added theorem Nat.ArithmeticFunction.coe_inj

added theorem Nat.ArithmeticFunction.coe_mk

added theorem Nat.ArithmeticFunction.coe_moebius_mul_coe_zeta

added theorem Nat.ArithmeticFunction.coe_mul_zeta_apply

added theorem Nat.ArithmeticFunction.coe_zetaUnit

added theorem Nat.ArithmeticFunction.coe_zeta_mul_apply

added theorem Nat.ArithmeticFunction.coe_zeta_mul_coe_moebius

added theorem Nat.ArithmeticFunction.coe_zeta_mul_moebius

added theorem Nat.ArithmeticFunction.coe_zeta_smul_apply

added theorem Nat.ArithmeticFunction.ext

added theorem Nat.ArithmeticFunction.ext_iff

added def Nat.ArithmeticFunction.id

added theorem Nat.ArithmeticFunction.id_apply

added theorem Nat.ArithmeticFunction.intCoe_apply

added theorem Nat.ArithmeticFunction.intCoe_int

added theorem Nat.ArithmeticFunction.intCoe_mul

added theorem Nat.ArithmeticFunction.intCoe_one

added theorem Nat.ArithmeticFunction.inv_zetaUnit

added theorem Nat.ArithmeticFunction.isMultiplicative_id

added theorem Nat.ArithmeticFunction.isMultiplicative_moebius

added theorem Nat.ArithmeticFunction.isMultiplicative_one

added theorem Nat.ArithmeticFunction.isMultiplicative_pow

added theorem Nat.ArithmeticFunction.isMultiplicative_sigma

added theorem Nat.ArithmeticFunction.isMultiplicative_zeta

added theorem Nat.ArithmeticFunction.map_zero

added def Nat.ArithmeticFunction.moebius

added theorem Nat.ArithmeticFunction.moebius_apply_isPrimePow_not_prime

added theorem Nat.ArithmeticFunction.moebius_apply_of_squarefree

added theorem Nat.ArithmeticFunction.moebius_apply_one

added theorem Nat.ArithmeticFunction.moebius_apply_prime

added theorem Nat.ArithmeticFunction.moebius_apply_prime_pow

added theorem Nat.ArithmeticFunction.moebius_eq_zero_of_not_squarefree

added theorem Nat.ArithmeticFunction.moebius_mul_coe_zeta

added theorem Nat.ArithmeticFunction.moebius_ne_zero_iff_eq_or

added theorem Nat.ArithmeticFunction.moebius_ne_zero_iff_squarefree

added theorem Nat.ArithmeticFunction.mul_apply

added theorem Nat.ArithmeticFunction.mul_apply_one

added theorem Nat.ArithmeticFunction.mul_smul'

added theorem Nat.ArithmeticFunction.mul_zeta_apply

added theorem Nat.ArithmeticFunction.natCoe_apply

added theorem Nat.ArithmeticFunction.natCoe_mul

added theorem Nat.ArithmeticFunction.natCoe_nat

added theorem Nat.ArithmeticFunction.natCoe_one

added def Nat.ArithmeticFunction.natToArithmeticFunction

added def Nat.ArithmeticFunction.ofInt

added theorem Nat.ArithmeticFunction.one_apply

added theorem Nat.ArithmeticFunction.one_apply_ne

added theorem Nat.ArithmeticFunction.one_one

added theorem Nat.ArithmeticFunction.one_smul'

added def Nat.ArithmeticFunction.pmul

added theorem Nat.ArithmeticFunction.pmul_apply

added theorem Nat.ArithmeticFunction.pmul_comm

added theorem Nat.ArithmeticFunction.pmul_zeta

added def Nat.ArithmeticFunction.pow

added theorem Nat.ArithmeticFunction.pow_apply

added theorem Nat.ArithmeticFunction.pow_zero_eq_zeta

added def Nat.ArithmeticFunction.ppow

added theorem Nat.ArithmeticFunction.ppow_apply

added theorem Nat.ArithmeticFunction.ppow_succ'

added theorem Nat.ArithmeticFunction.ppow_succ

added theorem Nat.ArithmeticFunction.ppow_zero

added theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq

added theorem Nat.ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero

added def Nat.ArithmeticFunction.sigma

added theorem Nat.ArithmeticFunction.sigma_apply

added theorem Nat.ArithmeticFunction.sigma_one_apply

added theorem Nat.ArithmeticFunction.sigma_zero_apply

added theorem Nat.ArithmeticFunction.sigma_zero_apply_prime_pow

added theorem Nat.ArithmeticFunction.smul_apply

added theorem Nat.ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq

added theorem Nat.ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq

added theorem Nat.ArithmeticFunction.toFun_eq

added theorem Nat.ArithmeticFunction.zero_apply

added def Nat.ArithmeticFunction.zeta

added def Nat.ArithmeticFunction.zetaUnit

added theorem Nat.ArithmeticFunction.zeta_apply

added theorem Nat.ArithmeticFunction.zeta_apply_ne

added theorem Nat.ArithmeticFunction.zeta_mul_apply

added theorem Nat.ArithmeticFunction.zeta_mul_pow_eq_sigma

added theorem Nat.ArithmeticFunction.zeta_pmul

added def Nat.ArithmeticFunction