Commit 2024-07-31 09:27 591bab05

View on Github →

feat(FieldTheory/IntermediateField): add Subfield.extendScalars (#15148) ... which can be viewed as an inverse to IntermediateField.toSubfield. This is similar to IntermediateField.extendScalars.

Estimated changes

Modified Mathlib/FieldTheory/IntermediateField.lean

modified def IntermediateField.extendScalars

added theorem Subfield.coe_extendScalars

added def Subfield.extendScalars.orderIso

added def Subfield.extendScalars

added theorem Subfield.extendScalars_injective

added theorem Subfield.extendScalars_le_extendScalars_iff

added theorem Subfield.extendScalars_le_iff

added theorem Subfield.extendScalars_toSubfield

added theorem Subfield.le_extendScalars_iff

added theorem Subfield.mem_extendScalars