Stars and bars, good first project

Stream: general

[Yaël Dillies]

I just opened issue #10802 as a good-first-project for the stars and bars theorem. This boils down to showing

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

I expect it to be very doable.

Bhavik and I already proved the case n = 2 (formally, card α = 2) in #8426.

[Huỳnh Trần Khanh]

interesting :joy: I want to work on this lemma, do I need write access or can I just fork and PR?

[Yaël Dillies]

Just fork and PR! But also you can give us your Github username and we'll add you to the repo.

[Huỳnh Trần Khanh]

it's huynhtrankhanh :heart: