Commit 2025-04-24 04:08 dadd3dae

View on Github →

chore(RingTheory): equivalence between algebraicity over IntermediateField.adjoin and Algebra.adjoin (#24004)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

modified theorem Subalgebra.coe_inclusion

modified theorem Subalgebra.inclusion_inclusion

modified theorem Subalgebra.inclusion_injective

modified theorem Subalgebra.inclusion_mk

modified theorem Subalgebra.inclusion_right

modified theorem Subalgebra.inclusion_self

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

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

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

added theorem IntermediateField.mem_adjoin_iff_div

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/RingTheory/Algebraic/Integral.lean

added theorem Algebra.IsAlgebraic.isAlgebraic_iff_bot

added theorem Algebra.IsAlgebraic.isAlgebraic_iff_top

added theorem Algebra.IsIntegral.isAlgebraic_iff_top

modified theorem Transcendental.extendScalars

modified theorem Transcendental.extendScalars_of_isIntegral

modified theorem Transcendental.subalgebraAlgebraicClosure

Modified Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean

added theorem IntermediateField.algebraicIndependent_adjoin_iff

added theorem IntermediateField.isAlgebraic_adjoin_iff

added theorem IntermediateField.isAlgebraic_adjoin_iff_bot

added theorem IntermediateField.isAlgebraic_adjoin_iff_top

added theorem IntermediateField.isTranscendenceBasis_adjoin_iff

added theorem IntermediateField.transcendental_adjoin_iff

Modified Mathlib/RingTheory/Localization/FractionRing.lean

added theorem IsFractionRing.of_field