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

Equations
Instances For
instance Finsupp.instHasAntidiagonal {α : Type u} [] :

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

Equations
• Finsupp.instHasAntidiagonal = { antidiagonal := fun (f : α →₀ ) => .support, mem_antidiagonal := }
@[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.1 p.2) = Finset.sum fun (p : (α →₀ ) × (α →₀ )) => f p.2 p.1
theorem Finsupp.prod_antidiagonal_swap {α : Type u} [] {M : Type u_1} [] (n : α →₀ ) (f : (α →₀ )(α →₀ )M) :
(Finset.prod fun (p : (α →₀ ) × (α →₀ )) => f p.1 p.2) = Finset.prod fun (p : (α →₀ ) × (α →₀ )) => f p.2 p.1
@[simp]
theorem Finsupp.antidiagonal_single {α : Type u} [] (a : α) (n : ) :
= Finset.map (Function.Embedding.prodMap { toFun := , inj' := } { toFun := , inj' := })