Commit 2024-10-18 15:39 9e3fa1e4

View on Github →

feat(FieldTheory/Adjoin): add some results of extendScalars (#15238)

extendScalars_{self|top|inf|sup} for intermediate fields and subfields
also add restrictScalars_{inf|sup} and bot_toSubfield
add a missing helper lemma toSubfield_injective

Estimated changes

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.bot_toSubfield

added theorem IntermediateField.extendScalars_inf

added theorem IntermediateField.extendScalars_self

added theorem IntermediateField.extendScalars_sup

added theorem IntermediateField.extendScalars_top

added theorem IntermediateField.restrictScalars_inf

added theorem IntermediateField.restrictScalars_sup

modified theorem IntermediateField.restrictScalars_top

added theorem Subfield.extendScalars_inf

added theorem Subfield.extendScalars_self

added theorem Subfield.extendScalars_sup

added theorem Subfield.extendScalars_top

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

modified theorem IntermediateField.map_injective

modified theorem IntermediateField.toSubalgebra_injective

added theorem IntermediateField.toSubfield_injective