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

s.antidiagonal = quot.lift_on s (λ (l : list α), ↑((multiset.powerset_aux l).revzip)) multiset.antidiagonal._proof_1

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 : multiset α × multiset α} :

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

@[simp]

theorem multiset.antidiagonal_cons {α : Type u_1} (a : α) (s : multiset α) :

@[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 : α → β} :