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.NatAntidiagonal and is further refined by file Data.Finset.NatAntidiagonal.

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)

@[simp]

theorem Multiset.Nat.mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ Multiset.Nat.antidiagonal n ↔ x.1 + x.2 = n

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

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

@[simp]

theorem Multiset.Nat.antidiagonal_zero : Multiset.Nat.antidiagonal 0 = {(0, 0)}

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

@[simp]

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

The antidiagonal of n does not contain duplicate entries.

@[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)

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)

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)

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