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.

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.
Instances For
    @[simp]
    theorem Multiset.mem_antidiagonal {α : Type u_1} {s : Multiset α} {x : Multiset α × Multiset α} :
    x Multiset.antidiagonal s x.fst + x.snd = s

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

    @[simp]
    @[simp]
    theorem Multiset.card_antidiagonal {α : Type u_1} (s : Multiset α) :
    Multiset.card (Multiset.antidiagonal s) = 2 ^ Multiset.card s
    theorem Multiset.prod_map_add {α : Type u_1} {β : Type u_2} [CommSemiring β] {s : Multiset α} {f : αβ} {g : αβ} :