mathlib3 documentation


Antidiagonals in ℕ × ℕ as finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the antidiagonals of ℕ × ℕ as finsets: the n-th antidiagonal is the finset 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 files data.list.nat_antidiagonal and data.multiset.nat_antidiagonal.

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


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


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


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

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

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

theorem finset.nat.antidiagonal.fst_le {n : } {kl : × } (hlk : kl finset.nat.antidiagonal n) :
kl.fst n
theorem finset.nat.antidiagonal.snd_le {n : } {kl : × } (hlk : kl finset.nat.antidiagonal n) :
kl.snd n
theorem finset.nat.filter_fst_eq_antidiagonal (n m : ) :
finset.filter (λ (x : × ), x.fst = m) (finset.nat.antidiagonal n) = ite (m n) {(m, n - m)}
theorem finset.nat.filter_snd_eq_antidiagonal (n m : ) :
finset.filter (λ (x : × ), x.snd = m) (finset.nat.antidiagonal n) = ite (m n) {(n - m, m)}

The disjoint union of antidiagonals Σ (n : ℕ), antidiagonal n is equivalent to the product ℕ × ℕ. This is such an equivalence, obtained by mapping (n, (k, l)) to (k, l).