The "antidiagonal" {(0,n), (1,n-1), ..., (n,0)} as a multiset.
The antidiagonal of a natural number n is
the multiset of pairs (i,j) such that i+j = n.
Equations
@[simp]
The cardinality of the antidiagonal of n is n+1.
@[simp]
The antidiagonal of 0 is the list [(0,0)]
@[simp]
The antidiagonal of n does not contain duplicate entries.