mathlib documentation

data.multiset.nat_antidiagonal

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

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

Equations
@[simp]

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]

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

@[simp]

The antidiagonal of n does not contain duplicate entries.