mathlib documentation

data.sym.card

Stars and bars #

In this file, we prove the case n = 2 of stars and bars.

Informal statement #

If we have n objects to put in k boxes, we can do so in exactly (n + k - 1).choose n ways.

Formal statement #

We can identify the k boxes with the elements of a fintype α of card k. Then placing n elements in those boxes corresponds to choosing how many of each element of α appear in a multiset of card n. sym α n being the subtype of multiset α of multisets of card n, writing stars and bars using types gives

-- TODO: this lemma is not yet proven
lemma stars_and_bars {α : Type*} [fintype α] (n : ) :
  card (sym α n) = (card α + n - 1).choose (card α) := sorry

TODO #

Prove the general case of stars and bars.

Tags #

stars and bars

theorem sym2.card_image_diag {α : Type u_1} [decidable_eq α] (s : finset α) :

The diag of s : finset α is sent on a finset of sym2 α of card s.card.

theorem sym2.card_image_off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :

The off_diag of s : finset α is sent on a finset of sym2 α of card s.off_diag.card / 2. This is because every element ⟦(x, y)⟧ of sym2 α not on the diagonal comes from exactly two pairs: (x, y) and (y, x).

theorem sym2.card_subtype_diag {α : Type u_1} [decidable_eq α] [fintype α] :
theorem sym2.card_subtype_not_diag {α : Type u_1} [decidable_eq α] [fintype α] :
theorem sym2.card {α : Type u_1} [decidable_eq α] [fintype α] :