mathlib3 documentation

data.finsupp.antidiagonal

The finsupp counterpart of multiset.antidiagonal. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
noncomputable def finsupp.antidiagonal' {α : Type u_1} (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
source
noncomputable def finsupp.antidiagonal {α : Type u_1} (f : α →₀ ℕ) :
finset ((α →₀ ℕ) × (α →₀ ℕ))

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

Equations
source
@[simp]
theorem finsupp.mem_antidiagonal {α : Type u_1} {f : α →₀ ℕ} {p : (α →₀ ℕ) × (α →₀ ℕ)} :
p ∈ f.antidiagonal ↔ p.fst + p.snd = f
source
theorem finsupp.swap_mem_antidiagonal {α : Type u_1} {n : α →₀ ℕ} {f : (α →₀ ℕ) × (α →₀ ℕ)} :
f.swap ∈ n.antidiagonal ↔ f ∈ n.antidiagonal
source
theorem finsupp.antidiagonal_filter_fst_eq {α : Type u_1} (f g : α →₀ ℕ) [D : Π (p : (α →₀ ℕ) × (α →₀ ℕ)), decidable (p.fst = g)] :
finset.filter (λ (p : (α →₀ ℕ) × (α →₀ ℕ)), p.fst = g) f.antidiagonal = ite (g ≤ f) {(g, f - g)} ∅
source
theorem finsupp.antidiagonal_filter_snd_eq {α : Type u_1} (f g : α →₀ ℕ) [D : Π (p : (α →₀ ℕ) × (α →₀ ℕ)), decidable (p.snd = g)] :
finset.filter (λ (p : (α →₀ ℕ) × (α →₀ ℕ)), p.snd = g) f.antidiagonal = ite (g ≤ f) {(f - g, g)} ∅
source
@[simp]
theorem finsupp.antidiagonal_zero {α : Type u_1} :
0.antidiagonal = {(0, 0)}
source
theorem finsupp.sum_antidiagonal_swap {α : Type u_1} {M : Type u_2} [add_comm_monoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
n.antidiagonal.sum (λ (p : (α →₀ ℕ) × (α →₀ ℕ)), f p.fst p.snd) = n.antidiagonal.sum (λ (p : (α →₀ ℕ) × (α →₀ ℕ)), f p.snd p.fst)
source
theorem finsupp.prod_antidiagonal_swap {α : Type u_1} {M : Type u_2} [comm_monoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
n.antidiagonal.prod (λ (p : (α →₀ ℕ) × (α →₀ ℕ)), f p.fst p.snd) = n.antidiagonal.prod (λ (p : (α →₀ ℕ) × (α →₀ ℕ)), f p.snd p.fst)