Commit 2024-01-19 16:10 50388bcc

View on Github →

feat({Ring|Field}Theory/Adjoin): add various results on adjoin (#9790) Main changes:

for intermediate fields: add extendScalars_adjoin, restrictScalars_adjoin_of_algEquiv, sup_toSubalgebra_of_isAlgebraic, adjoin_toSubalgebra_of_isAlgebraic, adjoin_rank_le_of_isAlgebraic, and golf sup_toSubalgebra
for subalgebras: add adjoin_eq_span_of_eq_span, adjoin_eq_span_basis, restrictScalars_adjoin, restrictScalars_adjoin_of_algEquiv, adjoin_rank_le

Estimated changes

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.adjoin_rank_le_of_isAlgebraic

added theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_left

added theorem IntermediateField.adjoin_rank_le_of_isAlgebraic_right

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.extendScalars_adjoin

added theorem IntermediateField.restrictScalars_adjoin_of_algEquiv

deleted theorem IntermediateField.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

Modified Mathlib/RingTheory/Adjoin/Basic.lean

added theorem Algebra.restrictScalars_adjoin

added theorem Algebra.restrictScalars_adjoin_of_algEquiv

added theorem Subalgebra.adjoin_eq_span_basis

added theorem Subalgebra.adjoin_eq_span_of_eq_span

added theorem Submonoid.adjoin_eq_span_of_eq_span

Modified Mathlib/RingTheory/Adjoin/Field.lean

added theorem Subalgebra.adjoin_rank_le