Bell Numbers count Partitions

Stream: mathlib4

[Eduardo]

Hello everyone, this is my first message here and I'm really glad to be finally participating in this community.

Among other things, I'm really interested in combinatorics, so I was excited when I realized mathlib didn't yet include a proof that bell numbers count partitions. I do see that we have Multibell numbers since even Finsets are still implemented as Multisets first, but yeah, the correspondence between multibell numbers and multiset partitions hasn't yet been established.

I already have an almost complete proof that the standard bell numbers count partitions of Finsets! And I'm really excited I managed to get there, but I want to understand how can I contribute this to Mathlib. Of course I can try enhancing the proof to be more general and consider multisets, but more than that I want to know if there are any naming conventions, or maybe line of code metric (my proof is currently around 700 lines) that I need to satisfy, or if maybe I need to be more through in reusing other results already in mathlib etc

Also, more on proof structure, I want to understand if it's ok to use simp, or if I need to always use simp only, and in general what constitutes a clean proof that's up to mathlib standards

I'm open to feedback and I already expect to hear that my Lean is not that good yet, but I really want to start contributing to mathlib so I don't mind: Partition.lean

(also I know that there's already a partition struct in mathlib but this one is simpler I think as it's just for finsets? Tho I'm not sure)

Thanks so much for your help

[Antoine Chambert-Loir]

Your link leads to 404.

[Antoine Chambert-Loir]

This is a nice result. There are summaries of mathlib's naming conventions and programming rules on mathlib's main page :

• Library style guidelines
• Naming conventions

[Eduardo]

oopsie sorry repo is public now

[Eduardo]

ok I realize now a few things:

1. the partition on Enumerative is integer partition, not set partition, I got confused (especially considering Bell is there as well). I realize now that I probably should use Data.Setoid.Partition
2. Since there's a TODO on Setoid.Partition my argument could be around Order.Partition.Finpartition instead, but I would have it to specialize to Fintypes anyways.
3. Considering I could generalize it for Multiset instead (to complete the TODO on Bell) that's already many different paths I go through

would appreciate some input on how to go about this on the cleanest way