Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-08 15:40 9b0d30c0

View on Github →

feat(number_theory/arithmetic_function): define is_multiplicative on arithmetic_functions, provides examples (#4312) Provides a few basic examples of important arithmetic functions Defines what it means for an arithmetic function to be multiplicative

Estimated changes

Modified src/data/nat/gcd.lean

added theorem nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul

Modified src/number_theory/arithmetic_function.lean

modified theorem nat.arithmetic_function.add_apply

modified theorem nat.arithmetic_function.coe_coe

modified theorem nat.arithmetic_function.coe_inj

modified theorem nat.arithmetic_function.ext

modified theorem nat.arithmetic_function.ext_iff

added def nat.arithmetic_function.id

added theorem nat.arithmetic_function.id_apply

modified theorem nat.arithmetic_function.int_coe_apply

added theorem nat.arithmetic_function.is_multiplicative.int_cast

added theorem nat.arithmetic_function.is_multiplicative.map_mul_of_coprime

added theorem nat.arithmetic_function.is_multiplicative.map_one

added theorem nat.arithmetic_function.is_multiplicative.mul

added theorem nat.arithmetic_function.is_multiplicative.nat_cast

added theorem nat.arithmetic_function.is_multiplicative.pmul

added theorem nat.arithmetic_function.is_multiplicative.ppow

added def nat.arithmetic_function.is_multiplicative

added theorem nat.arithmetic_function.is_multiplicative_id

added theorem nat.arithmetic_function.is_multiplicative_pow

added theorem nat.arithmetic_function.is_multiplicative_sigma

added theorem nat.arithmetic_function.is_multiplicative_zeta

modified theorem nat.arithmetic_function.map_zero

modified theorem nat.arithmetic_function.mul_apply

added theorem nat.arithmetic_function.mul_zeta_apply

modified theorem nat.arithmetic_function.nat_coe_apply

modified theorem nat.arithmetic_function.one_apply_ne

modified theorem nat.arithmetic_function.one_one

added def nat.arithmetic_function.pmul

added theorem nat.arithmetic_function.pmul_apply

added theorem nat.arithmetic_function.pmul_comm

added theorem nat.arithmetic_function.pmul_zeta

added def nat.arithmetic_function.pow

added theorem nat.arithmetic_function.pow_apply

added def nat.arithmetic_function.ppow

added theorem nat.arithmetic_function.ppow_apply

added theorem nat.arithmetic_function.ppow_succ'

added theorem nat.arithmetic_function.ppow_succ

added theorem nat.arithmetic_function.ppow_zero

added def nat.arithmetic_function.sigma

added theorem nat.arithmetic_function.sigma_apply

modified theorem nat.arithmetic_function.to_fun_eq

modified theorem nat.arithmetic_function.zero_apply

added def nat.arithmetic_function.zeta

added theorem nat.arithmetic_function.zeta_apply

added theorem nat.arithmetic_function.zeta_apply_ne

added theorem nat.arithmetic_function.zeta_mul_apply

added theorem nat.arithmetic_function.zeta_mul_pow_eq_sigma

added theorem nat.arithmetic_function.zeta_pmul

modified structure nat.arithmetic_function

Modified src/number_theory/divisors.lean

modified def nat.divisors

deleted theorem nat.divisors_eq_proper_divisors_insert_self

added theorem nat.divisors_eq_proper_divisors_insert_self_of_pos

modified theorem nat.divisors_zero

modified def nat.proper_divisors