Commit 2025-01-10 18:59 b6263152

View on Github →

refactor(IntermediateField/Adjoin): Split off relation to Algebra.adjoin (#20630) Part of IntermediateField/Adjoin/Basic is about the relation with Algebra.adjoin (e.g., assuming integrality). This PR splits off those results into their own file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

added theorem IntermediateField.AdjoinSimple.isIntegral_gen

added theorem IntermediateField.adjoin_algebraic_toSubalgebra

added theorem IntermediateField.adjoin_eq_algebra_adjoin

added theorem IntermediateField.adjoin_eq_top_of_algebra

added theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral

added theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic

added theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left

added theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right

added theorem IntermediateField.algebra_adjoin_le_adjoin

added theorem IntermediateField.eq_adjoin_of_eq_algebra_adjoin

added theorem IntermediateField.fg_of_fg_toSubalgebra

added theorem IntermediateField.fg_of_noetherian

added theorem IntermediateField.induction_on_adjoin

added theorem IntermediateField.le_sup_toSubalgebra

added theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic

added theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_left

added theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_right

added theorem IntermediateField.sup_toSubalgebra_of_left

added theorem IntermediateField.sup_toSubalgebra_of_right

added theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq

added theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq

added theorem IsFractionRing.liftAlgHom_fieldRange

added theorem IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

deleted theorem IntermediateField.AdjoinSimple.isIntegral_gen

deleted theorem IntermediateField.adjoin_algebraic_toSubalgebra

deleted theorem IntermediateField.adjoin_eq_algebra_adjoin

deleted theorem IntermediateField.adjoin_eq_top_of_algebra

deleted theorem IntermediateField.adjoin_rootSet_isSplittingField

deleted theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral

deleted theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic

deleted theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left

deleted theorem IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right

deleted theorem IntermediateField.algebra_adjoin_le_adjoin

deleted theorem IntermediateField.eq_adjoin_of_eq_algebra_adjoin

deleted theorem IntermediateField.fg_of_fg_toSubalgebra

deleted theorem IntermediateField.fg_of_noetherian

deleted theorem IntermediateField.induction_on_adjoin

deleted theorem IntermediateField.isSplittingField_iff

deleted theorem IntermediateField.le_sup_toSubalgebra

deleted theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic

deleted theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_left

deleted theorem IntermediateField.sup_toSubalgebra_of_isAlgebraic_right

deleted theorem IntermediateField.sup_toSubalgebra_of_left

deleted theorem IntermediateField.sup_toSubalgebra_of_right

deleted theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq

deleted theorem IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq

deleted theorem IsFractionRing.liftAlgHom_fieldRange

deleted theorem IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq

deleted theorem isSplittingField_iff_intermediateField

Modified Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

added theorem IntermediateField.adjoin_rootSet_isSplittingField

added theorem IntermediateField.isSplittingField_iff

added theorem isSplittingField_iff_intermediateField

Modified Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean