Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-02 16:48 41811cdd

View on Github →

feat(number_theory): von Mangoldt function (#11727) Defines the von Mangoldt function

Estimated changes

Modified src/algebra/is_prime_pow.lean

added theorem is_prime_pow_pow_iff

added theorem nat.coprime.is_prime_pow_dvd_mul

added theorem nat.disjoint_divisors_filter_prime_pow

added theorem nat.mul_divisors_filter_prime_pow

Modified src/number_theory/divisors.lean

added theorem nat.prod_divisors_antidiagonal'

added theorem nat.prod_divisors_antidiagonal

Created src/number_theory/von_mangoldt.lean

added theorem nat.arithmetic_function.log_apply

added theorem nat.arithmetic_function.log_mul_moebius_eq_von_mangoldt

added theorem nat.arithmetic_function.moebius_mul_log_eq_von_mangoldt

added theorem nat.arithmetic_function.sum_moebius_mul_log_eq

added theorem nat.arithmetic_function.von_mangoldt_apply

added theorem nat.arithmetic_function.von_mangoldt_apply_one

added theorem nat.arithmetic_function.von_mangoldt_apply_pow

added theorem nat.arithmetic_function.von_mangoldt_apply_prime

added theorem nat.arithmetic_function.von_mangoldt_mul_zeta

added theorem nat.arithmetic_function.von_mangoldt_nonneg

added theorem nat.arithmetic_function.von_mangoldt_sum

added theorem nat.arithmetic_function.zeta_mul_von_mangoldt