# mathlibdocumentation

data.finset.nat_antidiagonal

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

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

Equations
@[simp]
theorem finset.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]
theorem finset.nat.card_antidiagonal (n : ) :
= n + 1

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

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

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

theorem finset.nat.antidiagonal_congr {n : } {p q : × } (hp : p ) (hq : q ) :
p = q p.fst = q.fst

A point in the antidiagonal is determined by its first co-ordinate.