feat(FieldTheory/SeparableDegree): basic definition of separable degr…

…ee of field extension (#8117)

Main changes:

- rename current `Mathlib/FieldTheory/SeparableDegree` to `Mathlib/RingTheory/Polynomial/SeparableDegree`
  and create new `Mathlib/FieldTheory/SeparableDegree`

Main definitions

- `Emb F E`: the type of `F`-algebra homomorphisms from `E` to the algebraic closure of `E`.

- `sepDegree F E`: the separable degree of an algebraic extension `E / F` of fields, defined to be the cardinal of `F`-algebra homomorphisms from `E` to the algebraic closure of `E`. 
(Mathematically, it should be the algebraic closure of `F`, but in order to make the type compatible with `Module.rank F E`, we use the algebraic closure of `E`.)
  Note that if `E / F` is not algebraic, then this definition makes no mathematical sense.

- `finSepDegree F E`: the separable degree of `E / F` as a natural number, which is zero if `sepDegree F E` is not finite.

Main results

- `embEquivOfEquiv`, `sepDegree_eq_of_equiv`, `finSepDegree_eq_of_equiv`: a random isomorphism
  between `Emb F E` and `Emb F E'` when `E` and `E'` are isomorphic as `F`-algebras.
  In particular, they have the same cardinality (so `sepDegree` and `finSepDegree` are equal).

- `embEquivOfAdjoinSplits'`, `sepDegree_eq_of_adjoin_splits'`, `finSepDegree_eq_of_adjoin_splits'`:
  a random isomorphism between `Emb F E` and `E →ₐ[F] K` if `E = F(S)` such that every element
  `s` of `S` is integral (= algebraic) over `F` and whose minimal polynomial splits in `K`.
  In particular, they have the same cardinality.

- `embEquivOfIsAlgClosed`, `sepDegree_eq_of_isAlgClosed`, `finSepDegree_eq_of_isAlgClosed`:
  a random isomorphism between `Emb F E` and `E →ₐ[F] K` when `E / F`
  is algebraic and `K / F` is algebraically closed.
  In particular, they have the same cardinality.

- `embProdEmbOfIsAlgebraic`, `lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`,
  `sepDegree_mul_sepDegree_of_isAlgebraic`, `finSepDegree_mul_finSepDegree_of_isAlgebraic`:
  if `K / E / F` is a field extension tower, such that `K / E` is algebraic,
  then there is a non-canonical isomorphism `(Emb F E) × (Emb E K) ≃ (Emb F K)`.
  In particular, the separable degree satisfies the tower law: `[E:F]_s [K:E]_s = [K:F]_s`.

Mathlib.lean

@@ -3073,6 +3073,7 @@ import Mathlib.RingTheory.Polynomial.Quotient
 import Mathlib.RingTheory.Polynomial.RationalRoot
 import Mathlib.RingTheory.Polynomial.ScaleRoots
 import Mathlib.RingTheory.Polynomial.Selmer
+import Mathlib.RingTheory.Polynomial.SeparableDegree
 import Mathlib.RingTheory.Polynomial.Tower
 import Mathlib.RingTheory.Polynomial.Vieta
 import Mathlib.RingTheory.PolynomialAlgebra