The Finsupp counterpart of Multiset.antidiagonal.

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

noncomputable def Finsupp.antidiagonal' {α : Type u} [DecidableEq α] (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

• f.antidiagonal' = Multiset.toFinsupp (Multiset.map (Prod.map ⇑Multiset.toFinsupp ⇑Multiset.toFinsupp) (Finsupp.toMultiset f).antidiagonal)

@[instance_reducible]

noncomputable instance Finsupp.instHasAntidiagonal {α : Type u} [DecidableEq α] : Finset.HasAntidiagonal (α →₀ ℕ)

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

Equations

• Finsupp.instHasAntidiagonal = { antidiagonal := fun (f : α →₀ ℕ) => f.antidiagonal'.support, mem_antidiagonal := ⋯ }

@[simp]

theorem Finsupp.antidiagonal_zero {α : Type u} [DecidableEq α] : Finset.antidiagonal 0 = {(0, 0)}

theorem Finsupp.prod_antidiagonal_swap {α : Type u} [DecidableEq α] {M : Type u_1} [CommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) : ∏ p ∈ Finset.antidiagonal n, f p.1 p.2 = ∏ p ∈ Finset.antidiagonal n, f p.2 p.1

theorem Finsupp.sum_antidiagonal_swap {α : Type u} [DecidableEq α] {M : Type u_1} [AddCommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) : ∑ p ∈ Finset.antidiagonal n, f p.1 p.2 = ∑ p ∈ Finset.antidiagonal n, f p.2 p.1

@[simp]

theorem Finsupp.antidiagonal_single {α : Type u} [DecidableEq α] (a : α) (n : ℕ) : Finset.antidiagonal (single a n) = Finset.map ({ toFun := single a, inj' := ⋯ }.prodMap { toFun := single a, inj' := ⋯ }) (Finset.antidiagonal n)

theorem Finsupp.image_prodMap_embDomain_antidiagonal {α : Type u} [DecidableEq α] {β : Type u_1} [DecidableEq β] (f : α ↪ β) (y : α →₀ ℕ) : Finset.image (Prod.map (embDomain f) (embDomain f)) (Finset.antidiagonal y) = Finset.antidiagonal (embDomain f y)

theorem Finsupp.image_sumElim_product_antidiagonal {α : Type u} [DecidableEq α] {β : Type u_1} [DecidableEq β] {x : α →₀ ℕ} {y : β →₀ ℕ} : Finset.image (fun (x : ((α →₀ ℕ) × (α →₀ ℕ)) × (β →₀ ℕ) × (β →₀ ℕ)) => match x with | ((x, y), z, w) => (x.sumElim z, y.sumElim w)) (Finset.antidiagonal x ×ˢ Finset.antidiagonal y) = Finset.antidiagonal (x.sumElim y)