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.liftOn s (fun (l : List α) => ↑(Multiset.powersetAux l).revzip) ⋯
Instances For
theorem
Multiset.antidiagonal_coe
{α : Type u_1}
(l : List α)
:
(↑l).antidiagonal = ↑(Multiset.powersetAux l).revzip
@[simp]
theorem
Multiset.antidiagonal_coe'
{α : Type u_1}
(l : List α)
:
(↑l).antidiagonal = ↑(Multiset.powersetAux' l).revzip
@[simp]
theorem
Multiset.antidiagonal_map_fst
{α : Type u_1}
(s : Multiset α)
:
Multiset.map Prod.fst s.antidiagonal = s.powerset
@[simp]
theorem
Multiset.antidiagonal_map_snd
{α : Type u_1}
(s : Multiset α)
:
Multiset.map Prod.snd s.antidiagonal = s.powerset
@[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
theorem
Multiset.antidiagonal_eq_map_powerset
{α : Type u_1}
[DecidableEq α]
(s : Multiset α)
:
s.antidiagonal = Multiset.map (fun (t : Multiset α) => (s - t, t)) s.powerset
theorem
Multiset.prod_map_add
{α : Type u_1}
{β : Type u_2}
[CommSemiring β]
{s : Multiset α}
{f : α → β}
{g : α → β}
:
(Multiset.map (fun (a : α) => f a + g a) s).prod = (Multiset.map (fun (p : Multiset α × Multiset α) => (Multiset.map f p.1).prod * (Multiset.map g p.2).prod)
s.antidiagonal).sum