# Documentation

Mathlib.Data.Fin.Tuple.NatAntidiagonal

# 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 #

• List.Nat.antidiagonalTuple
• Multiset.Nat.antidiagonalTuple
• Finset.Nat.antidiagonalTuple

## Main results #

• antidiagonalTuple 2 n is analogous to antidiagonal n:

• List.Nat.antidiagonalTuple_two
• Multiset.Nat.antidiagonalTuple_two
• Finset.Nat.antidiagonalTuple_two

## Implementation notes #

While we could implement this by filtering (Fintype.PiFinset \$ fun _ ↦ range (n + 1)) or similar, this implementation would be much slower.

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

### Lists #

def List.Nat.antidiagonalTuple (k : ) :
List (Fin k)

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

This list contains no duplicates (List.Nat.nodup_antidiagonalTuple), and is sorted lexicographically (List.Nat.antidiagonalTuple_pairwise_pi_lex), starting with ![0, ..., n] and ending with ![n, ..., 0].

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

Equations
Instances For
theorem List.Nat.mem_antidiagonalTuple {n : } {k : } {x : Fin k} :
(Finset.sum Finset.univ fun i => x i) = n

The antidiagonal of n does not contain duplicate entries.

@[simp]
theorem List.Nat.antidiagonalTuple_one (n : ) :
= [![n]]
theorem List.Nat.antidiagonalTuple_two (n : ) :
= List.map (fun i => ![i.fst, i.snd]) ()
theorem List.Nat.antidiagonalTuple_pairwise_pi_lex (k : ) (n : ) :
List.Pairwise (Pi.Lex (fun x x_1 => x < x_1) fun x x x_1 => x < x_1) ()

### Multisets #

Multiset.Nat.antidiagonalTuple k n is a multiset of k-tuples summing to n

Instances For
theorem Multiset.Nat.mem_antidiagonalTuple {n : } {k : } {x : Fin k} :
(Finset.sum Finset.univ fun i => x i) = n
@[simp]
theorem Multiset.Nat.antidiagonalTuple_two (n : ) :
= Multiset.map (fun i => ![i.fst, i.snd]) ()

### Finsets #

Finset.Nat.antidiagonalTuple k n is a finset of k-tuples summing to n

Instances For
theorem Finset.Nat.mem_antidiagonalTuple {n : } {k : } {x : Fin k} :
(Finset.sum Finset.univ fun i => x i) = n
@[simp]
theorem Finset.Nat.antidiagonalTuple_one (n : ) :
= {![n]}
@[simp]
theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst (k : ) (x : Fin k) :
( x).fst = Finset.sum Finset.univ fun i => x i
@[simp]
theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe (k : ) (x : Fin k) :
∀ (a : Fin k), ( x).snd a = x a
@[simp]
theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_apply (k : ) (x : (n : ) × { x // }) :
∀ (a : Fin k), = x.snd a
def Finset.Nat.sigmaAntidiagonalTupleEquivTuple (k : ) :
(n : ) × { x // } (Fin k)

The disjoint union of antidiagonal tuples Σ n, antidiagonalTuple 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.sigmaAntidiagonalEquivProd.

Instances For