feat: cardinality of `Field.Emb` for infinite extensions

[alreadydone]

A construction by transfinite recursion, fairly standard in set theory, but I have yet to see similar arguments in mathlib. See module docstring for more details.

I use some ad hoc category theoretical definitions: IsNatEquiv is (Nat)Iso in the functor category, and inverseLimit is Functor.sections, but it may makes things unnecessarily complicated to use the category library (OrderDual would be needed for example), as the construction is fairly down to earth.

Zulip

---

I think @digama0 @sterraf @YaelDillies @vihdzp might be interested to review this. Are you aware of other similar proofs formalized in mathlib or elsewhere? Is there anything general (about the transfinite recursion setup?) that can be extracted?

Lots of notations are introduced as shorthands in the file; if you see a way to improve them, please let me know.

I now incline to put the majority of defs in a namespace (tentatively Field.Emb.Cardinal) rather than making them private, but that means there are lots of docstrings to add.

• [x] depends on: #9488
• [x] depends on: #11290