chore(SetTheory): split Cardinal/Basic.lean (leanprover-community#23014)

This PR splits `SetTheory.Cardinal.Basic` into three files:
* `Cardinal/Defs.lean`: definition of `Cardinal`, addition, zero, `א0`
* `Cardinal/Order.lean`: definition of pre/linear/wellorder on `Cardinal`, semiring and ordered semiring structures
* `Cardinal/Basic.lean`: leftovers, in particular finite/countable/small types and sets

In particular, `Defs.lean` defines cardinals without importing any algebra (measured with an `assert_not_exists Monoid`).

I would have liked to do more with `Cardinal/Order.lean` such as splitting it into a file focused more on the order and a file focused more on the arithmetic, but unfortunately the two are currently so interwoven that it would not make sense to break them apart. (It would require substantial redoing of proofs.) Even moving the `Preorder Cardinal` instance upstream is hard since it depends on Schröder-Bernstein which imports lots of algebra. It wouldn't actually help the imports much.

Author: Vierkantor

Mathlib.lean

@@ -5205,13 +5205,15 @@ import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.SetTheory.Cardinal.Cofinality
 import Mathlib.SetTheory.Cardinal.Continuum
 import Mathlib.SetTheory.Cardinal.CountableCover
+import Mathlib.SetTheory.Cardinal.Defs
 import Mathlib.SetTheory.Cardinal.Divisibility
 import Mathlib.SetTheory.Cardinal.ENat
 import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.SetTheory.Cardinal.Finsupp
 import Mathlib.SetTheory.Cardinal.Free
 import Mathlib.SetTheory.Cardinal.HasCardinalLT
 import Mathlib.SetTheory.Cardinal.NatCount
+import Mathlib.SetTheory.Cardinal.Order
 import Mathlib.SetTheory.Cardinal.Ordinal
 import Mathlib.SetTheory.Cardinal.Pigeonhole
 import Mathlib.SetTheory.Cardinal.Regular

Mathlib/Algebra/Polynomial/Roots.lean

@@ -8,7 +8,7 @@ import Mathlib.Algebra.Polynomial.RingDivision
 import Mathlib.Data.Set.Finite.Lemmas
 import Mathlib.RingTheory.Coprime.Lemmas
 import Mathlib.RingTheory.Localization.FractionRing
-import Mathlib.SetTheory.Cardinal.Basic
+import Mathlib.SetTheory.Cardinal.Order
 
 /-!
 # Theory of univariate polynomials

Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Combinatorics.SimpleGraph.Density
 import Mathlib.Data.Nat.Cast.Order.Field
 import Mathlib.Order.Partition.Equipartition
-import Mathlib.SetTheory.Cardinal.Basic
+import Mathlib.SetTheory.Cardinal.Order
 
 /-!
 # Graph uniformity and uniform partitions

Mathlib/Data/DFinsupp/WellFounded.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
 import Mathlib.Data.DFinsupp.Lex
-import Mathlib.Order.GameAdd
 import Mathlib.Order.Antisymmetrization
+import Mathlib.Order.GameAdd
+import Mathlib.SetTheory.Cardinal.Order
 import Mathlib.Tactic.AdaptationNote
-import Mathlib.SetTheory.Cardinal.Basic
 
 /-!
 # Well-foundedness of the lexicographic and product orders on `DFinsupp` and `Pi`

Mathlib/Order/Monotone/MonovaryOrder.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Order.Monotone.Monovary
-import Mathlib.SetTheory.Cardinal.Basic
+import Mathlib.SetTheory.Cardinal.Order
 
 /-!
 # Interpreting monovarying functions as monotone functions

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

@@ -8,8 +8,9 @@ import Mathlib.Algebra.GradedMonoid
 import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.Algebra.MvPolynomial.Equiv
 import Mathlib.Algebra.MvPolynomial.Variables
-import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 import Mathlib.Algebra.Polynomial.Roots
+import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
+import Mathlib.SetTheory.Cardinal.Basic
 
 /-!
 # Homogeneous polynomials

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -8,7 +8,7 @@ import Mathlib.SetTheory.Cardinal.Aleph
 /-!
 # Cardinal arithmetic
 
-Arithmetic operations on cardinals are defined in `SetTheory/Cardinal/Basic.lean`. However, proving
+Arithmetic operations on cardinals are defined in `SetTheory/Cardinal/Order.lean`. However, proving
 the important theorem `c * c = c` for infinite cardinals and its corollaries requires the use of
 ordinal numbers. This is done within this file.