The "antidiagonal" {(0,n), (1,n-1), ..., (n,0)} as a finset.
The antidiagonal of a natural number n is
the finset of pairs (i,j) such that i+j = n.
Equations
- finset.nat.antidiagonal n = {val := multiset.nat.antidiagonal n, nodup := _}
@[simp]
The cardinality of the antidiagonal of n is n+1.
@[simp]
The antidiagonal of 0 is the list [(0,0)]