# Documentation

Mathlib.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 : ) :

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

Equations
• One or more equations did not get rendered due to their size.
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 : } {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.map Prod.fst () =
@[simp]
theorem Multiset.antidiagonal_map_snd {α : Type u_1} (s : ) :
Multiset.map Prod.snd () =
@[simp]
theorem Multiset.antidiagonal_zero {α : Type u} :
= {(0, 0)}
@[simp]
theorem Multiset.antidiagonal_cons {α : Type u_1} (a : α) (s : ) :
theorem Multiset.antidiagonal_eq_map_powerset {α : Type u_1} [inst : ] (s : ) :
= Multiset.map (fun t => (s - t, t)) ()
@[simp]
theorem Multiset.card_antidiagonal {α : Type u_1} (s : ) :
Multiset.card () = 2 ^ Multiset.card s
theorem Multiset.prod_map_add {α : Type u_2} {β : Type u_1} [inst : ] {s : } {f : αβ} {g : αβ} :
Multiset.prod (Multiset.map (fun a => f a + g a) s) = Multiset.sum (Multiset.map (fun p => Multiset.prod (Multiset.map f p.fst) * Multiset.prod (Multiset.map g p.snd)) ())