The antidiagonal of a natural number n is the list of pairs (i,j) such that i+j = n.
Equations
- list.nat.antidiagonal n = list.map (λ (i : ℕ), (i, n - i)) (list.range (n + 1))
@[simp]
The length of the antidiagonal of n is n+1.
@[simp]
The antidiagonal of 0 is the list [(0,0)]
The antidiagonal of n does not contain duplicate entries.