Cardinality of the division ring generated by a set #

Subfield.cardinal_mk_closure_le_max: the cardinality of the (sub-)division ring generated by a set is bounded by the cardinality of the set unless it is finite.

The method used to prove this (via WType) can be easily generalized to other algebraic structures, but those cardinalities can usually be obtained by other means, using some explicit universal objects.