Antidiagonals in ℕ × ℕ as lists #
This file defines the antidiagonals of ℕ × ℕ as lists: the n
-th antidiagonal is the list of
pairs (i, j)
such that i + j = n
. This is useful for polynomial multiplication and more
generally for sums going from 0
to n
.
Notes #
Files Data.Multiset.NatAntidiagonal
and Data.Finset.NatAntidiagonal
successively turn the
List
definition we have here into Multiset
and Finset
.
@[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.