Commit 2024-04-14 08:49 f822da54

feat(NumberTheory/SmoothNumbers): add material on numbers with prime factors in a given Finset (#12055) As a preparation for refactoring Euler products to use the new infinite products, this PR generalizes Nat.smoothNumbers n to Nat.factoredNumbers s where s is a Finset of natural numbers; this is the set of all positive natural numbers all of whose prime factors are in s. We correspondingly generalize the API and use the new statements to golf the proofs of the old ones. (We also eliminate a few fairly slow converts and a tauto, so that the file should now be faster than before, even though it contains quite a few new declarations.) See here on Zulip.