# 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`.

source
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))

Instances For

source
@[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`.

source
@[simp]
theorem List.Nat.length_antidiagonal (n : ℕ) :
(antidiagonal n).length = n + 1

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

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

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

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

The antidiagonal of `n` does not contain duplicate entries.

source
@[simp]
theorem List.Nat.antidiagonal_succ {n : ℕ} :
antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)
source
theorem List.Nat.antidiagonal_succ' {n : ℕ} :
antidiagonal (n + 1) = map (Prod.map id Nat.succ) (antidiagonal n) ++ [(n + 1, 0)]
source
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)]
source
theorem List.Nat.map_swap_antidiagonal {n : ℕ} :
map Prod.swap (antidiagonal n) = (antidiagonal n).reverse