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.

def List.Nat.antidiagonal (n : ℕ) : List (ℕ × ℕ)

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 (fun (i : ℕ) => (i, n - i)) (List.range (n + 1))

@[simp]

theorem List.Nat.mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ 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.

@[simp]

theorem List.Nat.length_antidiagonal (n : ℕ) : (antidiagonal n).length = n + 1

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

@[simp]

theorem List.Nat.antidiagonal_zero : antidiagonal 0 = [(0, 0)]

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

theorem List.Nat.nodup_antidiagonal (n : ℕ) : (antidiagonal n).Nodup

The antidiagonal of n does not contain duplicate entries.

@[simp]

theorem List.Nat.antidiagonal_succ {n : ℕ} : antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)

theorem List.Nat.antidiagonal_succ' {n : ℕ} : antidiagonal (n + 1) = map (Prod.map id Nat.succ) (antidiagonal n) ++ [(n + 1, 0)]

theorem List.Nat.antidiagonal_succ_succ' {n : ℕ} : antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

theorem List.Nat.map_swap_antidiagonal {n : ℕ} : map Prod.swap (antidiagonal n) = (antidiagonal n).reverse