List.Nat.nodup_antidiagonalTuple

theorem List.Nat.nodup_antidiagonalTuple : ∀ (k n : ℕ), (List.Nat.antidiagonalTuple k n).Nodup

This theorem states that for any pair of natural numbers 'k' and 'n', the antidiagonal tuple of 'k' and 'n' has no duplicate entries. In other words, all elements in the antidiagonal tuple created from the given pair of natural numbers are unique.

More concisely: For all natural numbers k and n, the antidiagonal elements of the k x n matrix are distinct.