Commit 2023-10-31 06:01 85a1f28f

feat(Data.Finset.Antidiagonal): generalize Finset.Nat.antidiagonal (#7486) We define a type class Finset.HasAntidiagonal A which contains a function antidiagonal : A → Finset (A × A) such that antidiagonal n is the Finset of all pairs adding to n, as witnessed by mem_antidiagonal. When A is a canonically ordered add monoid with locally finite order this typeclass can be instantiated with Finset.antidiagonalOfLocallyFinite. This applies in particular when A is ℕ, more generally or σ →₀ ℕ, or even ι →₀ A under the additional assumption OrderedSub A that make it a canonically ordered add monoid. (In fact, we would just need an AddMonoid with a compatible order, finite Iic, such that if a + b = n, then a, b ≤ n, and any finiteness condition would be OK.) For computational reasons it is better to manually provide instances for ℕ and σ →₀ ℕ, to avoid quadratic runtime performance. These instances are provided as Finset.Nat.instHasAntidiagonal and Finsupp.instHasAntidiagonal. This is why Finset.antidiagonalOfLocallyFinite is an abbrev and not an instance. This definition does not exactly match with that of Multiset.antidiagonal defined in Mathlib.Data.Multiset.Antidiagonal, because of the multiplicities. Indeed, by counting multiplicities, Multiset α is equivalent to α →₀ ℕ, but Finset.antidiagonal and Multiset.antidiagonal will return different objects. For example, for s : Multiset ℕ := {0,0,0}, Multiset.antidiagonal s has 8 elements but Finset.antidiagonal s has only 4.

def s : Multiset ℕ := {0, 0, 0}
#eval (Finset.antidiagonal s).card -- 4
#eval Multiset.card (Multiset.antidiagonal s) -- 8

TODO

• Define HasMulAntidiagonal (for monoids). For PNat, we will recover the set of divisors of a strictly positive integer. This closes #7917 Co-authored by: María Inés de Frutos-Fernández mariaines.dff@gmail.com and Eric Wieser efw27@cam.ac.uk