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

Instances For
@[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_succ_succ' {n : } :
Finset.Nat.antidiagonal (n + 2) = Finset.cons (0, n + 2) (Finset.cons (n + 2, 0) (Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) ()) (_ : ¬(n + 2, 0) Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) ())) (_ : ¬(0, n + 2) Finset.cons (n + 2, 0) (Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) ()) (_ : ¬(n + 2, 0) Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) ()))
@[simp]
theorem Finset.Nat.map_swap_antidiagonal {n : } :
Finset.map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } () =

See also Finset.map.map_prodComm_antidiagonal.

@[simp]
theorem Finset.Nat.antidiagonal_congr {n : } {p : } {q : } (hp : ) (hq : ) :
p = q p.fst = q.fst

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

theorem Finset.Nat.antidiagonal_subtype_ext {n : } {p : { x // }} {q : { x // }} (h : (p).fst = (q).fst) :
p = q

A point in the antidiagonal is determined by its first co-ordinate (subtype version of antidiagonal_congr). This lemma is used by the ext tactic.

theorem Finset.Nat.antidiagonal.fst_le {n : } {kl : } (hlk : ) :
kl.fst n
theorem Finset.Nat.antidiagonal.fst_lt {n : } {kl : } (hlk : ) :
kl.fst < n + 1
theorem Finset.Nat.antidiagonal.snd_le {n : } {kl : } (hlk : ) :
kl.snd n
theorem Finset.Nat.antidiagonal.snd_lt {n : } {kl : } (hlk : ) :
kl.snd < n + 1
theorem Finset.Nat.filter_fst_eq_antidiagonal (n : ) (m : ) :
Finset.filter (fun x => x.fst = m) () = if m n then {(m, n - m)} else
theorem Finset.Nat.filter_snd_eq_antidiagonal (n : ) (m : ) :
Finset.filter (fun x => x.snd = m) () = if m n then {(n - m, m)} else
@[simp]
theorem Finset.Nat.antidiagonal_filter_snd_le_of_le {n : } {k : } (h : k n) :
Finset.filter (fun a => a.snd k) () = Finset.map (Function.Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Function.Injective fun x => x + (n - k)) } ()) ()
@[simp]
theorem Finset.Nat.antidiagonal_filter_fst_le_of_le {n : } {k : } (h : k n) :
Finset.filter (fun a => a.fst k) () = Finset.map (Function.Embedding.prodMap () { toFun := fun x => x + (n - k), inj' := (_ : Function.Injective fun x => x + (n - k)) }) ()
@[simp]
theorem Finset.Nat.antidiagonal_filter_le_fst_of_le {n : } {k : } (h : k n) :
Finset.filter (fun a => k a.fst) () = Finset.map (Function.Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Function.Injective fun x => x + k) } ()) (Finset.Nat.antidiagonal (n - k))
@[simp]
theorem Finset.Nat.antidiagonal_filter_le_snd_of_le {n : } {k : } (h : k n) :
Finset.filter (fun a => k a.snd) () = Finset.map (Function.Embedding.prodMap () { toFun := fun x => x + k, inj' := (_ : Function.Injective fun x => x + k) }) (Finset.Nat.antidiagonal (n - k))
@[simp]
theorem Finset.Nat.sigmaAntidiagonalEquivProd_apply (x : (n : ) × { x // }) :
@[simp]
theorem Finset.Nat.sigmaAntidiagonalEquivProd_symm_apply_fst (x : ) :
().fst = x.fst + x.snd

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

Instances For
@[simp]
theorem Finset.Nat.antidiagonalEquivFin_symm_apply_coe (n : ) :
∀ (x : Fin (n + 1)), ↑(().symm x) = (x, n - x)
@[simp]
theorem Finset.Nat.antidiagonalEquivFin_apply_val (n : ) :
∀ (x : { x // }), ↑() = x.1.fst
def Finset.Nat.antidiagonalEquivFin (n : ) :
{ x // } Fin (n + 1)

The set antidiagonal n is equivalent to Fin (n+1), via the first projection. -

Instances For