# mathlib3documentation

data.multiset.antidiagonal

# The antidiagonal on a multiset. #

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

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
theorem multiset.antidiagonal_coe {α : Type u_1} (l : list α) :
@[simp]
theorem multiset.antidiagonal_coe' {α : Type u_1} (l : list α) :
@[simp]
theorem multiset.mem_antidiagonal {α : Type u_1} {s : multiset α} {x : × } :
x.fst + x.snd = s

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

@[simp]
theorem multiset.antidiagonal_map_fst {α : Type u_1} (s : multiset α) :
@[simp]
theorem multiset.antidiagonal_map_snd {α : Type u_1} (s : multiset α) :
@[simp]
theorem multiset.antidiagonal_zero {α : Type u_1} :
0.antidiagonal = {(0, 0)}
@[simp]
theorem multiset.antidiagonal_cons {α : Type u_1} (a : α) (s : multiset α) :
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.card_antidiagonal {α : Type u_1} (s : multiset α) :
theorem multiset.prod_map_add {α : Type u_1} {β : Type u_2} {s : multiset α} {f g : α β} :
(multiset.map (λ (a : α), f a + g a) s).prod = (multiset.map (λ (p : × multiset α), p.fst).prod * p.snd).prod) s.antidiagonal).sum