Commit 2024-04-18 03:58 aa4476a8

feat(NumberTheory/EulerProduct/Basic): use infinite products, golf (#12161) This adds versions of the various Euler product statements in terms of the new topological products, namely HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n) and ∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n (and similar for completely multiplicative f in terms of (1 - f p)⁻¹). At the same time, I have reworked the proofs to some extent (in particular removing a few slow converts). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop). Unfortunately, this means that the diff is fairly large. See here and here on Zulip.