Commit 2024-11-14 11:04 4c452d85

feat(NumberTheory/EulerProduct/ExpLog): new file (#18923) This is the first PR in a series that will add proofs of the relevant properties of certain functions that are important for the proof of a density version of Dirichlet's Theorem on primes in AP (and, as a corollary, the Prime Number Theorem). Here we add a short new file with "logarithmic" versions of the Euler product of a completely multiplicative function. From EulerProducts.