Design theory in mathlib4

Stream: mathlib4

[Kevin Cheung]

I looked under Combinatorics and there doesn't seem to be a category for the theory of designs. Is anyone at the moment actively building a library of results in this area?

[Yaël Dillies]

All that's been done is Fisher's inequality by @Bhavik Mehta

[Kevin Cheung]

I see. So at the moment, if I start building basic things, I likely won't be wasting my effort.

[Kevin Cheung]

BTW, where does Fisher's inequality reside in mathlib4? A simple search on Fisher doesn't seem to return anything relevant.

[Yaël Dillies]

I think it was never ported from Lean 3, but it should be pretty easy

[Kevin Cheung]

Thanks. So Lean 3 does have some stuff on Design Theory?

[Yaël Dillies]

No, Bhavik did the design-less proof

[Kevin Cheung]

Thank you. I guess this is where I can put some work in.