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.

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

@[deprecated Subfield.cardinalMk_closure_le_max (since := "2024-11-10")]

theorem Subfield.cardinal_mk_closure_le_max {α : Type u} (s : Set α) [DivisionRing α] : Cardinal.mk ↥(closure s) ≤ Cardinal.mk ↑s ⊔ Cardinal.aleph0

Alias of Subfield.cardinalMk_closure_le_max.

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

@[deprecated Subfield.cardinalMk_closure (since := "2024-11-10")]

theorem Subfield.cardinal_mk_closure {α : Type u} (s : Set α) [DivisionRing α] [Infinite ↑s] : Cardinal.mk ↥(closure s) = Cardinal.mk ↑s

Alias of Subfield.cardinalMk_closure.