mathlib documentation

data.multiset.nat_antidiagonal

The "antidiagonal" {(0,n), (1,n-1), ..., (n,0)} as a multiset.

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
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.nat.antidiagonal n).card = 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)