Commit 2023-11-19 10:08 e49b5d07

View on Github →

feat(NumberTheory/EulerProduct): general statements about Euler products (#8410) This adds a folder NumberTheory.EulerProduct and within it the file Basic.lean, which contains some general results on Euler products (for functions from the naturals into a complete normed field, with suitable properties).

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/EulerProduct/Basic.lean

added theorem EulerProduct.eulerProduct

added theorem EulerProduct.eulerProduct_completely_multiplicative

added theorem EulerProduct.norm_tsum_smoothNumbers_sub_tsum_lt

added theorem EulerProduct.prod_primesBelow_geometric_eq_tsum_smoothNumbers

added theorem EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers

added theorem EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric

added theorem EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum

added theorem Summable.norm_lt_one

Modified Mathlib/NumberTheory/SmoothNumbers.lean

added theorem Nat.map_prime_pow_mul