Commit 2020-11-27 09:16 c06c6169

View on Github →

feat(number_theory/arithmetic_function): Moebius inversion (#5047) Changes the way that zeta works with coercion Proves Möbius inversion for functions to a general comm_ring

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.sum_int_cast

Modified src/number_theory/arithmetic_function.lean

modified theorem nat.arithmetic_function.coe_coe

added theorem nat.arithmetic_function.coe_moebius_mul_coe_zeta

added theorem nat.arithmetic_function.coe_mul_zeta_apply

added theorem nat.arithmetic_function.coe_zeta_mul_apply

added theorem nat.arithmetic_function.coe_zeta_mul_coe_moebius

added theorem nat.arithmetic_function.coe_zeta_mul_moebius

added theorem nat.arithmetic_function.coe_zeta_unit

modified theorem nat.arithmetic_function.int_coe_apply

added theorem nat.arithmetic_function.int_coe_int

added theorem nat.arithmetic_function.inv_zeta_unit

modified theorem nat.arithmetic_function.is_multiplicative_zeta

added theorem nat.arithmetic_function.moebius_mul_coe_zeta

deleted theorem nat.arithmetic_function.moebius_mul_zeta

modified theorem nat.arithmetic_function.mul_zeta_apply

modified theorem nat.arithmetic_function.nat_coe_apply

added theorem nat.arithmetic_function.nat_coe_nat

modified theorem nat.arithmetic_function.pmul_zeta

added theorem nat.arithmetic_function.sum_eq_iff_sum_moebius_eq

modified def nat.arithmetic_function.zeta

modified theorem nat.arithmetic_function.zeta_apply

modified theorem nat.arithmetic_function.zeta_apply_ne

modified theorem nat.arithmetic_function.zeta_mul_apply

deleted theorem nat.arithmetic_function.zeta_mul_moebius

modified theorem nat.arithmetic_function.zeta_pmul

added def nat.arithmetic_function.zeta_unit