mathlib documentation

data.multiset.antidiagonal

The antidiagonal on a multiset. #

The antidiagonal of a multiset s consists of all pairs (t₁, t₂) such that t₁ + t₂ = s. These pairs are counted with multiplicities.

source
def multiset.antidiagonal {α : Type u_1} (s : multiset α) :
multiset (multiset α × multiset α)

The antidiagonal of a multiset s consists of all pairs (t₁, t₂) such that t₁ + t₂ = s. These pairs are counted with multiplicities.

Equations
source
theorem multiset.antidiagonal_coe {α : Type u_1} (l : list α) :
↑l.antidiagonal = ↑((multiset.powerset_aux l).revzip)
source
@[simp]
theorem multiset.antidiagonal_coe' {α : Type u_1} (l : list α) :
↑l.antidiagonal = ↑((multiset.powerset_aux' l).revzip)
source
@[simp]
theorem multiset.mem_antidiagonal {α : Type u_1} {s : multiset α} {x : multiset α × multiset α} :
x ∈ s.antidiagonal ↔ x.fst + x.snd = s

A pair (t₁, t₂) of multisets is contained in antidiagonal s if and only if t₁ + t₂ = s.

source
@[simp]
theorem multiset.antidiagonal_map_fst {α : Type u_1} (s : multiset α) :
multiset.map prod.fst s.antidiagonal = s.powerset
source
@[simp]
theorem multiset.antidiagonal_map_snd {α : Type u_1} (s : multiset α) :
multiset.map prod.snd s.antidiagonal = s.powerset
source
@[simp]
theorem multiset.antidiagonal_zero {α : Type u_1} :
0.antidiagonal = {(0, 0)}
source
@[simp]
theorem multiset.antidiagonal_cons {α : Type u_1} (a : α) (s : multiset α) :
(a ::ₘ s).antidiagonal = multiset.map (prod.map id (multiset.cons a)) s.antidiagonal + multiset.map (prod.map (multiset.cons a) id) s.antidiagonal
source
@[simp]
theorem multiset.card_antidiagonal {α : Type u_1} (s : multiset α) :
⇑multiset.card s.antidiagonal = 2 ^ ⇑multiset.card s
source
theorem multiset.prod_map_add {α : Type u_1} {β : Type u_2} [comm_semiring β] {s : multiset α} {f g : α → β} :
(multiset.map (λ (a : α), f a + g a) s).prod = (multiset.map (λ (p : multiset α × multiset α), ((multiset.map f p.fst).prod) * (multiset.map g p.snd).prod) s.antidiagonal).sum