# Cardinality of the division ring generated by a set #

`Subfield.cardinalMk_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.

source
theorem Subfield.cardinalMk_closure_le_max {α : Type u} (s : Set α) [DivisionRing α] :
Cardinal.mk ↥(closure s) ≤ max (Cardinal.mk ↑s) Cardinal.aleph0
source
theorem Subfield.cardinalMk_closure {α : Type u} (s : Set α) [DivisionRing α] [Infinite ↑s] :
Cardinal.mk ↥(closure s) = Cardinal.mk ↑s