nodup_antidiagonalTuple — Mathlib

English

For all k and n, the multiset of all k-tuples of natural numbers summing to n has no duplicates.

Русский

Для всех k и n мультимножество всех k‑кортежей неотрицательных целых чисел суммой n не содержит повторяющихся элементов.

LaTeX

$$$ \operatorname{Nodup}\bigl(\operatorname{antidiagonalTuple}(k,n)\bigr). $$$

Lean4

theorem nodup_antidiagonalTuple (k n : ℕ) : (antidiagonalTuple k n).Nodup :=
  List.Nat.nodup_antidiagonalTuple _ _

Похожие утверждения