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.

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)
Instances For

    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.sum_antidiagonal_swap {α : Type u} [DecidableEq α] {M : Type u_1} [AddCommMonoid M] (n : α →₀ ) (f : (α →₀ )(α →₀ )M) :
    pFinset.antidiagonal n, f p.1 p.2 = pFinset.antidiagonal n, f p.2 p.1
    theorem Finsupp.prod_antidiagonal_swap {α : Type u} [DecidableEq α] {M : Type u_1} [CommMonoid M] (n : α →₀ ) (f : (α →₀ )(α →₀ )M) :
    pFinset.antidiagonal n, f p.1 p.2 = pFinset.antidiagonal n, f p.2 p.1
    @[simp]
    theorem Finsupp.antidiagonal_single {α : Type u} [DecidableEq α] (a : α) (n : ) :
    Finset.antidiagonal (Finsupp.single a n) = Finset.map ({ toFun := Finsupp.single a, inj' := }.prodMap { toFun := Finsupp.single a, inj' := }) (Finset.antidiagonal n)