# 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, providing an instance enabling Finset.antidiagonal on Nat.

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

Equations
theorem Finset.Nat.antidiagonal_eq_map (n : ) :
= Finset.map { toFun := fun (i : ) => (i, n - i), inj' := } (Finset.range (n + 1))
theorem Finset.Nat.antidiagonal_eq_map' (n : ) :
= Finset.map { toFun := fun (i : ) => (n - i, i), inj' := } (Finset.range (n + 1))
theorem Finset.Nat.antidiagonal_eq_image (n : ) :
= Finset.image (fun (i : ) => (i, n - i)) (Finset.range (n + 1))
theorem Finset.Nat.antidiagonal_eq_image' (n : ) :
= Finset.image (fun (i : ) => (n - i, i)) (Finset.range (n + 1))
@[simp]
theorem Finset.Nat.card_antidiagonal (n : ) :
.card = 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 (n : ) :
Finset.antidiagonal (n + 1) = Finset.cons (0, n + 1) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap ) )
theorem Finset.Nat.antidiagonal_succ' (n : ) :
Finset.antidiagonal (n + 1) = Finset.cons (n + 1, 0) (Finset.map (.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) )
theorem Finset.Nat.antidiagonal_succ_succ' {n : } :
Finset.antidiagonal (n + 2) = Finset.cons (0, n + 2) (Finset.cons (n + 2, 0) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) ) )
theorem Finset.Nat.antidiagonal.fst_lt {n : } {kl : } (hlk : ) :
kl.1 < n + 1
theorem Finset.Nat.antidiagonal.snd_lt {n : } {kl : } (hlk : ) :
kl.2 < n + 1
@[simp]
theorem Finset.Nat.antidiagonal_filter_snd_le_of_le {n : } {k : } (h : k n) :
Finset.filter (fun (a : ) => a.2 k) = Finset.map ({ toFun := fun (x : ) => x + (n - k), inj' := }.prodMap )
@[simp]
theorem Finset.Nat.antidiagonal_filter_fst_le_of_le {n : } {k : } (h : k n) :
Finset.filter (fun (a : ) => a.1 k) = Finset.map (.prodMap { toFun := fun (x : ) => x + (n - k), inj' := })
@[simp]
theorem Finset.Nat.antidiagonal_filter_le_fst_of_le {n : } {k : } (h : k n) :
Finset.filter (fun (a : ) => k a.1) = Finset.map ({ toFun := fun (x : ) => x + k, inj' := }.prodMap ) (Finset.antidiagonal (n - k))
@[simp]
theorem Finset.Nat.antidiagonal_filter_le_snd_of_le {n : } {k : } (h : k n) :
Finset.filter (fun (a : ) => k a.2) = Finset.map (.prodMap { toFun := fun (x : ) => x + k, inj' := }) (Finset.antidiagonal (n - k))
@[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.1
def Finset.Nat.antidiagonalEquivFin (n : ) :
{ x : // } Fin (n + 1)

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

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