Antidiagonals in ℕ × ℕ as multisets #

This file defines the antidiagonals of ℕ × ℕ as multisets: the n-th antidiagonal is the multiset 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 #

This refines file data.list.nat_antidiagonal and is further refined by file data.finset.nat_antidiagonal.

source

def multiset.nat.antidiagonal (n : ℕ) :

multiset (ℕ × ℕ)

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

Equations

multiset.nat.antidiagonal n = ↑(list.nat.antidiagonal n)

source

@[simp]

theorem multiset.nat.mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :

x ∈ multiset.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 multiset.nat.card_antidiagonal (n : ℕ) :

⇑multiset.card (multiset.nat.antidiagonal n) = n + 1

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

source

@[simp]

theorem multiset.nat.antidiagonal_zero :

multiset.nat.antidiagonal 0 = {(0, 0)}

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

source

@[simp]

theorem multiset.nat.nodup_antidiagonal (n : ℕ) :

(multiset.nat.antidiagonal n).nodup

The antidiagonal of n does not contain duplicate entries.

source

@[simp]

theorem multiset.nat.antidiagonal_succ {n : ℕ} :

multiset.nat.antidiagonal (n + 1) = (0, n + 1) ::ₘ multiset.map (prod.map nat.succ id) (multiset.nat.antidiagonal n)

source

theorem multiset.nat.antidiagonal_succ' {n : ℕ} :

multiset.nat.antidiagonal (n + 1) = (n + 1, 0) ::ₘ multiset.map (prod.map id nat.succ) (multiset.nat.antidiagonal n)

source

theorem multiset.nat.antidiagonal_succ_succ' {n : ℕ} :

multiset.nat.antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ multiset.map (prod.map nat.succ nat.succ) (multiset.nat.antidiagonal n)

source

theorem multiset.nat.map_swap_antidiagonal {n : ℕ} :

multiset.map prod.swap (multiset.nat.antidiagonal n) = multiset.nat.antidiagonal n