feat(FieldTheory): add basic api's for relative algebraic closure

[jjdishere]

Move the definition of algebraicClosure into a separated file (mimicing seperableClosure in file FieldTheory.SeperableClosure). Add APIs for algebraicClosure. Most are copied api's from separableClosure. Show that every algebraic intermediate extension is contained in the algebraic closure.

---

• [x] depends on: #14206

[github-actions[bot]]

PR summary 428cdfd57c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.FieldTheory.AlgebraicClosure	1356

---

Declarations diff

+ AlgEquiv.algebraicClosure + Algebra.IsAlgebraic.of_isIntegralClosure + IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic + IsAlgClosed.algebraicClosure_eq_bot_iff + adjoin_le + algEquivOfAlgEquiv + algebraicClosure_eq_bot + comap_eq_of_algHom + eq_restrictScalars_of_isAlgebraic + eq_top_iff + isAlgClosure + isAlgebraic + isIntegralClosure + le_algebraicClosure + le_algebraicClosure' + le_algebraicClosure_iff + le_restrictScalars + map_eq_of_algEquiv + map_eq_of_algebraicClosure_eq_bot + map_le_of_algHom + map_mem_algebraicClosure_iff + mem_algebraicClosure_iff + mem_algebraicClosure_iff' + ne_zero_iff + normalClosure_eq_self

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[jjdishere]

#14206 may overlap with this

Oops, sorry I didn't notice your PR. Thank you very much! @alreadydone

It seems that most of the lemmas are not overlapped, only the definition and several instances are overlapped. I am happy to modify my PR if yours is merged first.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#14206~~ By Dependent Issues (🤖). Happy coding!

[jjdishere]

One generic observation, not sure if it's something we should do: We could also define IntermediateField.algebraicClosure which takes an intermediate field E/K/F, and sends it to E/L/F, where L is the algebraic closure of K in F. The current definition would then be the special case algebraicClosure \bot. But if we don't have a use case for this, maybe we should ignore it 😄

Thank you for the suggestion! I believe there is currently no immediate need for IntermediateField.algebraicClosure. For now, it can be achieved by (algebraicClosure K F).restrictScalars E. If we are going to state lemmas in this form, it might be a suitable opportunity to generalize the definition.

[github-actions[bot]]

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

[mathlib-bors[bot]]

:v: jjdishere can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jjdishere]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build