feat: every nimber is between two groups/rings/fields

[plp127]

We prove every nimber not equal to zero is between two groups, which have no other groups in between.
We prove every nimber greater than one is between two rings/fields, which have no other rings/fields in between.

[vihdzp]

I wonder if a better approach would be to instead define the enumerator functions for groups/rings/fields, prove them normal, and get this as a corollary.

[plp127]

We could do that without much difficulty, but I don't think the enumerator functions would be generally useful, so I prefer not having them.

[vihdzp]

I think the fact that these enumerator functions exist and are normal (i.e. there is a proper class of groups/rings/fields) is interesting enough on its own. If you don't wanna do it I can open that PR instead.

[plp127]

Maybe it would be better to do all this in the generality of a closed unbounded set of ordinals? Or of any well-ordered set?

[vihdzp]

The existing API on club sets is... not good, unfortunately. The Mathlib.SetTheory.Ordinal.Topology file is a mess mostly of my own creation, and I've been trying to clean it up for a long while.

I do still think it'd be nice to have these enumerator functions. There are at least a few semi-interesting things to be said about them. For instance: if o is an uncountable initial ordinal, then the o-th group/ring/field/algebraically closed field is ∗o itself.