Monster files

Stream: general

[Yaël Dillies]

There are still a few monster files around. The first one that comes to mind is data.finset.basic. How should we slash it?

[Yaël Dillies]

I'm for removing the 150 lines or so about piecewise as it's not as used as the rest of the file and it's already well isolated.

[Yaël Dillies]

card as well is pretty well delimited and does make sense as a file on its own.

[Bryan Gin-ge Chen]

I haven't looked at the file in a while, but I'm all for splitting it up further!

[Yaël Dillies]

It just grows on its own :shrug: and I'm again about to feed the monster some more lemmas.

[Johan Commelin]

Do we already have group_theory.monster? That genuinely ought to be the only monster file in mathlib (_;

[Thomas Browning]

Maybe one more for the Tarski monster group