Stars and bars

[YaelDillies]

The stars and bars theorem should be doable with some finset fidgeting and double counting.

sym α n being the type of n elements of α without order, aka the n-th symmetric square on α. its cardinality is precisely what we want to count in stars and bars. Hence a neat way to state stars and bars would be

import data.sym.card

lemma stars_and_bars {α : Type*} [decidable_eq α] [fintype α] (n : ℕ) :
  fintype.card (sym α n) = (fintype.card α + n - 1).choose (fintype.card α) := sorry

The case n = 2 is already done in data.sym.card.

Zulip

[librarianmage]

Am I mistaken or has this already been proved by the above linked PRs?

[YaelDillies]

Indeed! It should have been closed along with the merge of #11162.