Commit 2024-11-23 06:30 f700f821

feat(FieldTheory): minimal polynomials determine an algebraic extension (Isaacs 1980) (#18412) If E/F is an algebraic extension and K/F is an arbitrary extension, and if the minimal polynomial of every element of E over F has a root in K, we show there exists an F-embedding from E into K. If E/F and K/F have the same set of minimal polynomials, they are then isomorphic. Another corollary is that an algebraic extension E/F is an algebraic closure if every (monic irreducible) polynomial in F[X] has a root in E. These results are proven in FieldTheory/Isaacs. An important definition (IsExtendible) and two important lemmas towards these theorems concern IntermediateField.Lifts and reside in FieldTheory/Extension. The lemmas say that the supremum of a chain of extendible lifts is also extendible, and that a lift with full domain exists if the bottom lift is extendible. We do slight refactoring to extract Lifts.union, and provide new API lemmas for Lifts.