Zulip Chat Archive

Stream: general

Topic: Stars and bars, good first project

Yaël Dillies (Dec 15 2021 at 00:36):

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 (Dec 15 2021 at 00:39):

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

Yaël Dillies (Dec 15 2021 at 00:40):

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 (Dec 15 2021 at 00:42):

it's huynhtrankhanh :heart:

Last updated: Aug 03 2023 at 10:10 UTC