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.
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 α) :
↑l.antidiagonal = ↑((multiset.powerset_aux l).revzip)
@[simp]
theorem
multiset.antidiagonal_coe'
{α : Type u_1}
(l : list α) :
↑l.antidiagonal = ↑((multiset.powerset_aux' l).revzip)
@[simp]
@[simp]
@[simp]
theorem
multiset.antidiagonal_cons
{α : Type u_1}
(a : α)
(s : multiset α) :
(a :: s).antidiagonal = multiset.map (prod.map id (multiset.cons a)) s.antidiagonal + multiset.map (prod.map (multiset.cons a) id) s.antidiagonal
@[simp]
theorem
multiset.card_antidiagonal
{α : Type u_1}
(s : multiset α) :
s.antidiagonal.card = 2 ^ s.card
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