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

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)

Instances For

source
@[simp]
theorem Multiset.Nat.mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :
x ∈ 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`.

source
@[simp]
theorem Multiset.Nat.card_antidiagonal (n : ℕ) :
(antidiagonal n).card = n + 1

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

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

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

source
@[simp]
theorem Multiset.Nat.nodup_antidiagonal (n : ℕ) :
(antidiagonal n).Nodup

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

source
@[simp]
theorem Multiset.Nat.antidiagonal_succ {n : ℕ} :
antidiagonal (n + 1) = (0, n + 1) ::ₘ map (Prod.map Nat.succ id) (antidiagonal n)
source
theorem Multiset.Nat.antidiagonal_succ' {n : ℕ} :
antidiagonal (n + 1) = (n + 1, 0) ::ₘ map (Prod.map id Nat.succ) (antidiagonal n)
source
theorem Multiset.Nat.antidiagonal_succ_succ' {n : ℕ} :
antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)
source
theorem Multiset.Nat.map_swap_antidiagonal {n : ℕ} :
map Prod.swap (antidiagonal n) = antidiagonal n