chore(set_theory/ordinal): split into multiple files (#3517)

Split the file `ordinal.lean` into three files, and add docstrings for all definitions and file-level docstrings. This is just shuffling things around: no new content, no erased content.


Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: sgouezel

src/data/real/cardinality.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 
 The cardinality of the reals.
 -/
-import set_theory.ordinal
+import set_theory.cardinal_ordinal
 import analysis.specific_limits
 import data.rat.denumerable
 import data.set.intervals.image_preimage

src/linear_algebra/dimension.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro, Johannes Hölzl, Sander Dahmen
 -/
 import linear_algebra.basis
-import set_theory.ordinal
+import set_theory.cardinal_ordinal
 
 /-!
 # Dimension of modules and vector spaces

src/set_theory/cardinal.lean

@@ -15,6 +15,11 @@ We define the order on cardinal numbers, define omega, and do basic cardinal ari
   addition, multiplication, power, cardinal successor, minimum, supremum,
     infinitary sums and products
 
+The fact that the cardinality of `α × α` coincides with that of `α` when `α` is infinite is not
+proved in this file, as it relies on facts on well-orders. Instead, it is in
+`cardinal_ordinal.lean` (together with many other facts on cardinals, for instance the
+cardinality of `list α`).
+
 ## Implementation notes
 
 * There is a type of cardinal numbers in every universe level: `cardinal.{u} : Type (u + 1)`

src/set_theory/cardinal_ordinal.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
 -/
-import set_theory.ordinal
+import set_theory.cardinal_ordinal
 /-!
 # Cofinality on ordinals, regular cardinals
 -/