Commit 2024-10-17 11:36 7d50a88f

View on Github →

feat(Algebra): integralClosure as IntermediateField (#14206)

Add lemmas about integrality and membership in an subalgebra of inverse elements.
As a consequence, show the integral closure of a field in a division ring is an intermediate field IntermediateField.algClosure.
Golf some lemmas along the way.

Estimated changes

Modified Mathlib/FieldTheory/Adjoin.lean

modified theorem IntermediateField.adjoin_le_iff

Modified Mathlib/FieldTheory/IntermediateField/Algebraic.lean

added theorem IntermediateField.coe_isIntegral_iff

modified theorem IntermediateField.isIntegral_iff

added def Subalgebra.IsAlgebraic.toIntermediateField

added def algebraicClosure

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

deleted theorem IntermediateField.coe_isIntegral_iff

Modified Mathlib/FieldTheory/PurelyInseparable.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

added theorem FiniteDimensional.isUnit

Modified Mathlib/RingTheory/Algebraic.lean

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean

added theorem AlgEquiv.isIntegral_iff

modified theorem Algebra.IsIntegral.of_injective

modified theorem IsIntegral.of_mem_of_fg

added theorem Subalgebra.isIntegral_iff

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

added theorem Algebra.IsIntegral.adjoin

added theorem Algebra.IsIntegral.inv_mem

added theorem Algebra.isIntegral_iSup

added theorem IsIntegral.inv

added theorem IsIntegral.inv_mem

added theorem IsIntegral.inv_mem_adjoin

added theorem IsIntegral.isUnit

added theorem IsIntegral.mem_of_inv_mem

added theorem IsIntegralClosure.isField

added theorem integralClosure_eq_top_iff

modified theorem isField_of_isIntegral_of_isField'