# mathlib3documentation

data.fin.tuple.nat_antidiagonal

# Collections of tuples of naturals with the same sum #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file generalizes list.nat.antidiagonal n, multiset.nat.antidiagonal n, and finset.nat.antidiagonal n from the pair of elements x : ℕ × ℕ such that n = x.1 + x.2, to the sequence of elements x : fin k → ℕ such that n = ∑ i, x i.

## Main definitions #

• list.nat.antidiagonal_tuple
• multiset.nat.antidiagonal_tuple
• finset.nat.antidiagonal_tuple

## Main results #

• antidiagonal_tuple 2 n is analogous to antidiagonal n:

• list.nat.antidiagonal_tuple_two
• multiset.nat.antidiagonal_tuple_two
• finset.nat.antidiagonal_tuple_two

## Implementation notes #

While we could implement this by filtering (fintype.pi_finset \$ λ _, range (n + 1)) or similar, this implementation would be much slower.

In the future, we could consider generalizing finset.nat.antidiagonal_tuple further to support finitely-supported functions, as is done with cut in archive/100-theorems-list/45_partition.lean.

### Lists #

list.antidiagonal_tuple k n is a list of all k-tuples which sum to n.

This list contains no duplicates (list.nat.nodup_antidiagonal_tuple), and is sorted lexicographically (list.nat.antidiagonal_tuple_pairwise_pi_lex), starting with ![0, ..., n] and ending with ![n, ..., 0].

#eval antidiagonal_tuple 3 2
-- [![0, 0, 2], ![0, 1, 1], ![0, 2, 0], ![1, 0, 1], ![1, 1, 0], ![2, 0, 0]]

Equations
@[simp]
theorem list.nat.mem_antidiagonal_tuple {n k : } {x : fin k } :
finset.univ.sum (λ (i : fin k), x i) = n

The antidiagonal of n does not contain duplicate entries.

@[simp]
theorem list.nat.antidiagonal_tuple_two (n : ) :
= list.map (λ (i : × ), ![i.fst, i.snd])

### Multisets #

multiset.antidiagonal_tuple k n is a multiset of k-tuples summing to n

Equations
@[simp]
theorem multiset.nat.mem_antidiagonal_tuple {n k : } {x : fin k } :
finset.univ.sum (λ (i : fin k), x i) = n

### Finsets #

finset.antidiagonal_tuple k n is a finset of k-tuples summing to n

Equations
@[simp]
theorem finset.nat.mem_antidiagonal_tuple {n k : } {x : fin k } :
finset.univ.sum (λ (i : fin k), x i) = n
@[simp]
theorem finset.nat.antidiagonal_tuple_one (n : ) :
= {![n]}
@[simp]
@[simp]
theorem finset.nat.sigma_antidiagonal_tuple_equiv_tuple_apply (k : ) (x : Σ (n : ), ) (ᾰ : fin k) :
= (x.snd) ᾰ

The disjoint union of antidiagonal tuples Σ n, antidiagonal_tuple k n is equivalent to the k-tuple fin k → ℕ. This is such an equivalence, obtained by mapping (n, x) to x.

This is the tuple version of finset.nat.sigma_antidiagonal_equiv_prod.

Equations