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.

The antidiagonal of a natural number n is the list of pairs (i, j) such that i + j = n.

Instances For
    theorem List.Nat.mem_antidiagonal {n : } {x : × } :
    x List.Nat.antidiagonal n x.fst + x.snd = n

    A pair (i, j) is contained in the antidiagonal of n if and only if i + j = n.


    The length of the antidiagonal of n is n + 1.


    The antidiagonal of 0 is the list [(0, 0)]

    The antidiagonal of n does not contain duplicate entries.