Commit 2024-11-28 15:29 0823ec54
View on Github →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)