Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-02 17:31 28031a80

View on Github →

feat(number_theory/factorization): evaluating arithmetic functions at prime powers (#13817)

Estimated changes

Modified archive/100-theorems-list/70_perfect_numbers.lean

Modified src/data/int/cast.lean

added theorem int.cast_ite

Modified src/data/list/dedup.lean

added theorem list.repeat_dedup

Modified src/number_theory/arithmetic_function.lean

added theorem nat.arithmetic_function.card_distinct_factors_apply_prime

added theorem nat.arithmetic_function.card_distinct_factors_apply_prime_pow

added theorem nat.arithmetic_function.card_distinct_factors_one

added theorem nat.arithmetic_function.card_factors_apply_prime

added theorem nat.arithmetic_function.card_factors_apply_prime_pow

modified theorem nat.arithmetic_function.coe_zeta_mul_coe_moebius

added theorem nat.arithmetic_function.int_coe_mul

added theorem nat.arithmetic_function.int_coe_one

added theorem nat.arithmetic_function.is_multiplicative_one

added theorem nat.arithmetic_function.moebius_apply_is_prime_pow_not_prime

modified theorem nat.arithmetic_function.moebius_apply_of_squarefree

added theorem nat.arithmetic_function.moebius_apply_one

added theorem nat.arithmetic_function.moebius_apply_prime

added theorem nat.arithmetic_function.moebius_apply_prime_pow

modified theorem nat.arithmetic_function.moebius_eq_zero_of_not_squarefree

added theorem nat.arithmetic_function.mul_apply_one

added theorem nat.arithmetic_function.nat_coe_mul

added theorem nat.arithmetic_function.nat_coe_one

added theorem nat.arithmetic_function.one_apply

modified theorem nat.arithmetic_function.one_apply_ne

modified theorem nat.arithmetic_function.one_one

added theorem nat.arithmetic_function.pow_zero_eq_zeta

modified theorem nat.arithmetic_function.sigma_one_apply

added theorem nat.arithmetic_function.sigma_zero_apply

added theorem nat.arithmetic_function.sigma_zero_apply_prime_pow