Commit 2024-11-28 15:29 0823ec54

feat: Define Nat.finMulAntidiagonal, the Finset of tuples of naturals with a fixed product. (#10668) The result card_finMulAntidiagonal_of_squarefree is central to controlling the error term in my formalisation of the Selberg sieve. (specifically for lemma 3.1 in Heath-Brown's notes) The definition is adapted from Finset.finAntidiagonal, though it is held back a bit by Nat.divisorsAntidiagonal which has a time complexity of $O(n^2)$. This definition is limited to Nat because it's not clear how to handle 0 in higher generality. (zulip)