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} :

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) ::ₘ 0

@[simp]
theorem multiset.card_antidiagonal {α : Type u_1} (s : multiset α) :

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