mathlib3 documentation

data.list.nat_antidiagonal

Antidiagonals in ℕ × ℕ as lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.nat_antidiagonal and data.finset.nat_antidiagonal 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
source
@[simp]
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.

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

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

source
@[simp]
theorem list.nat.antidiagonal_zero  :
list.nat.antidiagonal 0 = [(0, 0)]

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

source
theorem list.nat.nodup_antidiagonal (n : ℕ) :
(list.nat.antidiagonal n).nodup

The antidiagonal of n does not contain duplicate entries.

source
@[simp]
theorem list.nat.antidiagonal_succ {n : ℕ} :
list.nat.antidiagonal (n + 1) = (0, n + 1) :: list.map (prod.map nat.succ id) (list.nat.antidiagonal n)
source
theorem list.nat.antidiagonal_succ' {n : ℕ} :
list.nat.antidiagonal (n + 1) = list.map (prod.map id nat.succ) (list.nat.antidiagonal n) ++ [(n + 1, 0)]
source
theorem list.nat.antidiagonal_succ_succ' {n : ℕ} :
list.nat.antidiagonal (n + 2) = (0, n + 2) :: list.map (prod.map nat.succ nat.succ) (list.nat.antidiagonal n) ++ [(n + 2, 0)]
source
theorem list.nat.map_swap_antidiagonal {n : ℕ} :
list.map prod.swap (list.nat.antidiagonal n) = (list.nat.antidiagonal n).reverse