Polya's enumeration theorem

Stream: new members

[Abel Doñate Muñoz]

Hi, we are perhaps planning to formalize Polya's enumeration theorem. We saw there's a couple of PRs (#30525) (#31113) addressing this topic. Is there someone already doing this formalization project or should we start from scratch?