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.

def multiset.antidiagonal {α : Type u_1} (s : 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
@[simp]
@[simp]
theorem multiset.mem_antidiagonal {α : Type u_1} {s : multiset α} {x : multiset α × multiset α} :

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

@[simp]
@[simp]
@[simp]
theorem multiset.antidiagonal_zero {α : Type u_1} :
0.antidiagonal = {(0, 0)}
theorem multiset.antidiagonal_eq_map_powerset {α : Type u_1} [decidable_eq α] (s : multiset α) :
s.antidiagonal = multiset.map (λ (t : multiset α), (s - t, t)) s.powerset
@[simp]
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