mathlib documentation

data.fin.tuple.nat_antidiagonal

Collections of tuples of naturals with the same sum #

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 #

Main results #

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 #

def list.nat.antidiagonal_tuple (k : ) :
list (fin k)

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
theorem list.nat.mem_antidiagonal_tuple {n k : } {x : fin k} :

The antidiagonal of n does not contain duplicate entries.

Multisets #

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

Equations
theorem multiset.nat.mem_antidiagonal_tuple {n k : } {x : fin k} :

Finsets #

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

Equations
theorem finset.nat.mem_antidiagonal_tuple {n k : } {x : fin k} :

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