Commit 2023-05-30 09:32 541bcf2b

View on Github →

feat: port NumberTheory.VonMangoldt (#4494)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/VonMangoldt.lean

added theorem Nat.ArithmeticFunction.log_apply

added theorem Nat.ArithmeticFunction.log_mul_moebius_eq_vonMangoldt

added theorem Nat.ArithmeticFunction.moebius_mul_log_eq_vonMangoldt

added theorem Nat.ArithmeticFunction.sum_moebius_mul_log_eq

added theorem Nat.ArithmeticFunction.vonMangoldt_apply

added theorem Nat.ArithmeticFunction.vonMangoldt_apply_one

added theorem Nat.ArithmeticFunction.vonMangoldt_apply_pow

added theorem Nat.ArithmeticFunction.vonMangoldt_apply_prime

added theorem Nat.ArithmeticFunction.vonMangoldt_eq_zero_iff

added theorem Nat.ArithmeticFunction.vonMangoldt_le_log

added theorem Nat.ArithmeticFunction.vonMangoldt_mul_zeta

added theorem Nat.ArithmeticFunction.vonMangoldt_ne_zero_iff

added theorem Nat.ArithmeticFunction.vonMangoldt_nonneg

added theorem Nat.ArithmeticFunction.vonMangoldt_pos_iff

added theorem Nat.ArithmeticFunction.vonMangoldt_sum

added theorem Nat.ArithmeticFunction.zeta_mul_vonMangoldt