Documentation

Mathlib.Data.Finset.NatAntidiagonal

Antidiagonals in ℕ × ℕ as finsets #

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.NatAntidiagonal and Data.Multiset.NatAntidiagonal.

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

@[simp]

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

@[simp]

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.filter_fst_eq_antidiagonal (n : ) (m : ) :
Finset.filter (fun x => x.fst = m) (Finset.Nat.antidiagonal n) = if m n then {(m, n - m)} else
theorem Finset.Nat.filter_snd_eq_antidiagonal (n : ) (m : ) :
Finset.filter (fun x => x.snd = m) (Finset.Nat.antidiagonal n) = if m n then {(n - m, m)} else

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

Equations
  • One or more equations did not get rendered due to their size.