chore(RingTheory): split AlgebraicIndependent.lean

As a follow-up to splitting `RingTheory/Algebraic.lean`, also split `AlgebraicIndependent.lean`.

This PR creates the following new files:
* `AlgebraicIndependent/Defs.lean`: definition of `AlgebraicIndependent` and `IsTranscendenceBasis`
* `AlgebraicIndependent/Basic.lean`: basic results on `AlgebraicIndependent`
* `AlgebraicIndependent/TranscendenceBasis.lean`: basic results on `TranscendenceBasis`
* `AlgebraicIndependent/Adjoin.lean`: relating `AlgebraicIndependent` and `IntermediateField.adjoin`
* `AlgebraicIndependent/Transcendental.lean`: relating `AlgebraicIndependent`, `Transcendental` and `Algebraic`
* `AlgebraicIndependent/RankAndCardinality.lean`: about the rank/cardinality of `TranscendenceBasis`es

Mathlib.lean

@@ -4226,7 +4226,12 @@ import Mathlib.RingTheory.Algebraic.Integral
 import Mathlib.RingTheory.Algebraic.LinearIndependent
 import Mathlib.RingTheory.Algebraic.MvPolynomial
 import Mathlib.RingTheory.Algebraic.Pi
-import Mathlib.RingTheory.AlgebraicIndependent
+import Mathlib.RingTheory.AlgebraicIndependent.Adjoin
+import Mathlib.RingTheory.AlgebraicIndependent.Basic
+import Mathlib.RingTheory.AlgebraicIndependent.Defs
+import Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
+import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
+import Mathlib.RingTheory.AlgebraicIndependent.Transcendental
 import Mathlib.RingTheory.Artinian
 import Mathlib.RingTheory.Bezout
 import Mathlib.RingTheory.Bialgebra.Basic

Mathlib/FieldTheory/IsAlgClosed/Classification.lean

@@ -8,7 +8,7 @@ import Mathlib.Algebra.MvPolynomial.Cardinal
 import Mathlib.Algebra.Polynomial.Cardinal
 import Mathlib.FieldTheory.IsAlgClosed.Basic
 import Mathlib.RingTheory.Algebraic.Cardinality
-import Mathlib.RingTheory.AlgebraicIndependent
+import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
 
 /-!
 # Classification of Algebraically closed fields

Mathlib/FieldTheory/SeparableDegree.lean

@@ -7,7 +7,8 @@ import Mathlib.FieldTheory.SplittingField.Construction
 import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.NormalClosure
-import Mathlib.RingTheory.AlgebraicIndependent
+import Mathlib.RingTheory.AlgebraicIndependent.Adjoin
+import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
 import Mathlib.RingTheory.Polynomial.SeparableDegree
 import Mathlib.RingTheory.Polynomial.UniqueFactorization