# mathlibdocumentation

data.multiset.nat_antidiagonal

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

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

Equations
@[simp]
theorem multiset.nat.mem_antidiagonal {n : } {x : × } :
x.fst + x.snd = n

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

@[simp]

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

@[simp]
theorem multiset.nat.antidiagonal_zero  :
= {(0, 0)}

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

@[simp]

The antidiagonal of n does not contain duplicate entries.

@[simp]
theorem multiset.nat.antidiagonal_succ {n : } :
= (0, n + 1) ::ₘ