Commit 2020-12-02 07:25 61f63649

View on Github →

feat(number_theory/arithmetic_function): Möbius inversion for add_comm_groups, comm_groups (#5115) Adds scalar multiplication for arithmetic_functions Generalizes Möbius inversion to work with (add_)comm_groups

Estimated changes

Modified src/number_theory/arithmetic_function.lean

added theorem nat.arithmetic_function.coe_zeta_smul_apply

modified theorem nat.arithmetic_function.mul_apply

added theorem nat.arithmetic_function.mul_smul'

added theorem nat.arithmetic_function.one_smul'

added theorem nat.arithmetic_function.prod_eq_iff_prod_pow_moebius_eq

added theorem nat.arithmetic_function.smul_apply

deleted theorem nat.arithmetic_function.sum_eq_iff_sum_moebius_eq

added theorem nat.arithmetic_function.sum_eq_iff_sum_mul_moebius_eq

added theorem nat.arithmetic_function.sum_eq_iff_sum_smul_moebius_eq