[Merged by Bors] - feat(FieldTheory/PrimitiveElement): Steinitz Theorem

[acmepjz]

Added Field.exists_primitive_element_iff_finite_intermediateField: a finite extension E / F has a primitive element if and only if the intermediate fields between E / F are finitely many.
Also known as Steinitz Theorem https://en.wikipedia.org/wiki/Primitive_element_theorem#The_theorems.

---

• depends on: [Merged by Bors] - refactor(FieldTheory/Adjoin): provide a better defeq for ⊥ #7957

[alreadydone]

Will take a closer look later

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor(FieldTheory/Adjoin): provide a better defeq for ⊥ #7957
  By Dependent Issues (🤖). Happy coding!

[alreadydone]

Thanks, looks great to me now!

[acmepjz]

generalize to 0 ≤ m ≠ n;

I think this should be easy; I'll try it at next day.

show [F⟮α⟯ : F⟮α ^ m⟯] = m if m > 0 and α transcendental.

I think maybe you can prove directly that 1, α, ... , α ^ (m-1) form a basis of F⟮α⟯ as a F⟮α ^ m⟯-vector space?

Or perhaps more generally, [F⟮α⟯ : F⟮Polynomial.aeval α f⟯] = m if f : F[X] with m = f.natDegree > 0 and α transcendental

[alreadydone]

I think maybe you can prove directly that 1, α, ... , α ^ (m-1) form a basis of F⟮α⟯ as a F⟮α ^ m⟯-vector space?

Or perhaps more generally, [F⟮α⟯ : F⟮Polynomial.aeval α f⟯] = m if f : F[X] with m = f.natDegree > 0 and α transcendental

Yeah, both are true. A PowerBasis follows once you show irreducibility of the polynomial (which implies it's the minimal polynomial of α over F⟮α ^ m⟯). A direct proof of linear independence would also be feasible, more so for the similar statement about Algebra.adjoin, but for IntermediateField.adjoin you can still clear the denominators and the proof is essentially the same. I'm not sure it's easier than the proof using irreducibility though.

For the more general statement, actually you can take any rational function f/g in α, and the degree of the field extension of [F(α⟯ : F⟮f(α)/g(α)⟯] will be max {deg f, deg g} assuming f and g are coprime. For this general result, the Eisenstein criterion no longer applies, but there's actually a simpler proof that generalizes: wlog we may assume deg g < deg f because we may replace f/g by g/f, or in case deg f = deg g, replace it by 1/(f/g-1). We may further assume f is monic, so that the candidate minimal polynomial f(X)-g(X)Y of f(α)/g(α) is also monic as a polynomial in X, so we can use integral closedness of F[Y] to reduce irreducibility problem to the ring F[Y][X] as before. But this polynomial is of degree 1 in Y, so its factors are pretty easy to analyze: if it's a product then one of the factors must be of degree 0 in Y, so a polynomial in X, which must be a unit because it needs to divide both f and g.

[acmepjz]

Sorry for messing around with Adjoin. I added two new lemmas and make some of them simp lemmas. Is that OK?

[alreadydone]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Check all files imported
• Lint style
• Build