# Documentation

Mathlib.Data.Finsupp.Antidiagonal

# The Finsupp counterpart of Multiset.antidiagonal. #

The antidiagonal of s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.

def Finsupp.antidiagonal' {α : Type u} [] (f : α →₀ ) :

The Finsupp counterpart of Multiset.antidiagonal: the antidiagonal of s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s. The finitely supported function antidiagonal s is equal to the multiplicities of these pairs.

Instances For
def Finsupp.antidiagonal {α : Type u} [] (f : α →₀ ) :

The antidiagonal of s : α →₀ ℕ is the finset of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.

Instances For
@[simp]
theorem Finsupp.mem_antidiagonal {α : Type u} [] {f : α →₀ } {p : (α →₀ ) × (α →₀ )} :
p.fst + p.snd = f
theorem Finsupp.swap_mem_antidiagonal {α : Type u} [] {n : α →₀ } {f : (α →₀ ) × (α →₀ )} :
theorem Finsupp.antidiagonal_filter_fst_eq {α : Type u} [] (f : α →₀ ) (g : α →₀ ) [D : (p : (α →₀ ) × (α →₀ )) → Decidable (p.fst = g)] :
Finset.filter (fun p => p.fst = g) () = if g f then {(g, f - g)} else
theorem Finsupp.antidiagonal_filter_snd_eq {α : Type u} [] (f : α →₀ ) (g : α →₀ ) [D : (p : (α →₀ ) × (α →₀ )) → Decidable (p.snd = g)] :
Finset.filter (fun p => p.snd = g) () = if g f then {(f - g, g)} else
@[simp]
theorem Finsupp.antidiagonal_zero {α : Type u} [] :
= {(0, 0)}
theorem Finsupp.sum_antidiagonal_swap {α : Type u} [] {M : Type u_1} [] (n : α →₀ ) (f : (α →₀ ) → (α →₀ ) → M) :
(Finset.sum () fun p => f p.fst p.snd) = Finset.sum () fun p => f p.snd p.fst
theorem Finsupp.prod_antidiagonal_swap {α : Type u} [] {M : Type u_1} [] (n : α →₀ ) (f : (α →₀ ) → (α →₀ ) → M) :
(Finset.prod () fun p => f p.fst p.snd) = Finset.prod () fun p => f p.snd p.fst
@[simp]
theorem Finsupp.antidiagonal_single {α : Type u} [] (a : α) (n : ) :
(Finsupp.antidiagonal fun₀ | a => n) = Finset.map (Function.Embedding.prodMap { toFun := , inj' := (_ : ) } { toFun := , inj' := (_ : ) }) ()