English
The function antidiagonalTuple assigns to each natural numbers k and n the multiset of all k-tuples of natural numbers that sum to n, obtained from the list version by forgetting duplicates and ordering lexicographically.
Русский
Функция antidiagonalTuple назначает парам (k,n) мультимножество всех k-кубратов ℕ, сумма которых равна n, получаемое из списка без повторов и лексикографически упорядоченное.
LaTeX
$$$ \\mathrm{antidiagonalTuple}: \\mathbb{N}\\times\\mathbb{N} \\to \\mathrm{Multiset}(\\mathsf{Fin}\\,k \\to \\mathbb{N}) \\text{ — мультимножество всех k-кубратов, сумма которых равна } n $$$
Lean4
/-- `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]]
```
-/
def antidiagonalTuple : ∀ k, ℕ → List (Fin k → ℕ)
| 0, 0 => [![]]
| 0, _ + 1 => []
| k + 1, n => (List.Nat.antidiagonal n).flatMap fun ni => (antidiagonalTuple k ni.2).map fun x => Fin.cons ni.1 x
