The Finsupp counterpart of Multiset.antidiagonal. #
The antidiagonal of s : α →₀ ℕ consists of
all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.
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
- Finsupp.antidiagonal' f = Multiset.toFinsupp (Multiset.map (Prod.map ⇑Multiset.toFinsupp ⇑Multiset.toFinsupp) (Multiset.antidiagonal (Finsupp.toMultiset f)))
Instances For
The antidiagonal of s : α →₀ ℕ is the finset of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)
such that t₁ + t₂ = s.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Finsupp.sum_antidiagonal_swap
{α : Type u}
[DecidableEq α]
{M : Type u_1}
[AddCommMonoid M]
(n : α →₀ ℕ)
(f : (α →₀ ℕ) → (α →₀ ℕ) → M)
:
(Finset.sum (Finset.antidiagonal n) fun (p : (α →₀ ℕ) × (α →₀ ℕ)) => f p.1 p.2) = Finset.sum (Finset.antidiagonal n) fun (p : (α →₀ ℕ) × (α →₀ ℕ)) => f p.2 p.1
theorem
Finsupp.prod_antidiagonal_swap
{α : Type u}
[DecidableEq α]
{M : Type u_1}
[CommMonoid M]
(n : α →₀ ℕ)
(f : (α →₀ ℕ) → (α →₀ ℕ) → M)
:
(Finset.prod (Finset.antidiagonal n) fun (p : (α →₀ ℕ) × (α →₀ ℕ)) => f p.1 p.2) = Finset.prod (Finset.antidiagonal n) fun (p : (α →₀ ℕ) × (α →₀ ℕ)) => f p.2 p.1
@[simp]
theorem
Finsupp.antidiagonal_single
{α : Type u}
[DecidableEq α]
(a : α)
(n : ℕ)
:
Finset.antidiagonal (Finsupp.single a n) = Finset.map
(Function.Embedding.prodMap { toFun := Finsupp.single a, inj' := (_ : Function.Injective (Finsupp.single a)) }
{ toFun := Finsupp.single a, inj' := (_ : Function.Injective (Finsupp.single a)) })
(Finset.antidiagonal n)