Commit 2024-10-30 14:15 4b231df5

View on Github →

feat(FieldTheory): add basic api's for relative algebraic closure (#16771) 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.

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/AlgebraicClosure.lean

added theorem IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic

added theorem IsAlgClosed.algebraicClosure_eq_bot_iff

added theorem algebraicClosure.adjoin_le

added def algebraicClosure.algEquivOfAlgEquiv

added theorem algebraicClosure.algebraicClosure_eq_bot

added theorem algebraicClosure.comap_eq_of_algHom

added theorem algebraicClosure.eq_restrictScalars_of_isAlgebraic

added theorem algebraicClosure.eq_top_iff

added theorem algebraicClosure.le_restrictScalars

added theorem algebraicClosure.map_eq_of_algEquiv

added theorem algebraicClosure.map_eq_of_algebraicClosure_eq_bot

added theorem algebraicClosure.map_le_of_algHom

added theorem algebraicClosure.normalClosure_eq_self

added def algebraicClosure

added theorem le_algebraicClosure'

added theorem le_algebraicClosure

added theorem le_algebraicClosure_iff

added theorem map_mem_algebraicClosure_iff

added theorem mem_algebraicClosure_iff'

added theorem mem_algebraicClosure_iff

Modified Mathlib/FieldTheory/IntermediateField/Algebraic.lean

deleted def algebraicClosure

Modified Mathlib/FieldTheory/Minpoly/Basic.lean

added theorem minpoly.ne_zero_iff

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/Algebraic.lean

added theorem Algebra.IsAlgebraic.of_isIntegralClosure