Jiang Jiedong

> #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...

> 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`...

bors r+

> Doesn't [IntermediateField.splits_of_mem_adjoin](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Normal.html#IntermediateField.splits_of_mem_adjoin) directly imply the result in the title (and #17903)? Thank you very much @alreadydone ! I didn't find this theorem before. For those intermediate results in this...

@alreadydone I've checked the dependency. [IntermediateField.splits_of_mem_adjoin](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Normal.html#IntermediateField.splits_of_mem_adjoin) live in the file [FieldTheory.Normal](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Normal.html), which imports [FieldTheory.SplittingField.Construction](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/SplittingField/Construction.html), which imports [FieldTheory.SplittingField.IsSplittingField](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/SplittingField/IsSplittingField.html), which imports [RingTheory.Adjoin.Field](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Adjoin/Field.html), which is the file my theorems live in. So indeed...

bors r+

> Can you please fix the error? Thanks! Sorry for the delay! Fixed.

bors r+

For the natural lemma that is missing in this PR, which is `minpoly_algebraMap_sub_splits`, please see #17369 .