Commit 2023-05-23 11:55 9594d4af

View on Github →

feat: port FieldTheory.IntermediateField (#4258)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/IntermediateField.lean

added theorem AlgHom.coe_fieldRange

added def AlgHom.fieldRange

added theorem AlgHom.fieldRange_toSubfield

added theorem AlgHom.mem_fieldRange

added theorem IntermediateField.aeval_coe

added theorem IntermediateField.algebraMap_mem

added theorem IntermediateField.coe_copy

added theorem IntermediateField.coe_inclusion

added theorem IntermediateField.coe_isIntegral_iff

added theorem IntermediateField.coe_map

added theorem IntermediateField.coe_nat_mem

added theorem IntermediateField.coe_prod

added theorem IntermediateField.coe_restrictScalars

added theorem IntermediateField.coe_smul

added theorem IntermediateField.coe_sum

added theorem IntermediateField.coe_toSubalgebra

added theorem IntermediateField.coe_toSubfield

added theorem IntermediateField.coe_val

added theorem IntermediateField.copy_eq

added theorem IntermediateField.eq_of_le_of_finrank_eq'

added theorem IntermediateField.eq_of_le_of_finrank_eq

added theorem IntermediateField.eq_of_le_of_finrank_le'

added theorem IntermediateField.ext

added theorem IntermediateField.fieldRange_le

added theorem IntermediateField.fieldRange_val

added theorem IntermediateField.finrank_eq_finrank_subalgebra

added def IntermediateField.inclusion

added theorem IntermediateField.inclusion_inclusion

added theorem IntermediateField.inclusion_injective

added theorem IntermediateField.inclusion_self

added def IntermediateField.intermediateFieldMap

added theorem IntermediateField.intermediateFieldMap_apply_coe

added theorem IntermediateField.intermediateFieldMap_symm_apply_coe

added theorem IntermediateField.isAlgebraic_iff

added theorem IntermediateField.isIntegral_iff

added def IntermediateField.lift

added def IntermediateField.map

added theorem IntermediateField.map_map

added theorem IntermediateField.mem_carrier

added theorem IntermediateField.mem_mk

added theorem IntermediateField.mem_restrictScalars

added theorem IntermediateField.mem_toSubalgebra

added theorem IntermediateField.mem_toSubfield

added theorem IntermediateField.minpoly_eq

added theorem IntermediateField.range_val

added theorem IntermediateField.rank_eq_rank_subalgebra

added def IntermediateField.restrictScalars

added theorem IntermediateField.restrictScalars_injective

added theorem IntermediateField.restrictScalars_toSubalgebra

added theorem IntermediateField.restrictScalars_toSubfield

added theorem IntermediateField.set_range_subset

added theorem IntermediateField.smul_mem

added theorem IntermediateField.toSubalgebra_eq_iff

added theorem IntermediateField.toSubalgebra_injective

added theorem IntermediateField.toSubalgebra_le_toSubalgebra

added theorem IntermediateField.toSubalgebra_lt_toSubalgebra

added def IntermediateField.toSubfield

added def IntermediateField.val

added theorem IntermediateField.val_mk

added structure IntermediateField

added def Subalgebra.toIntermediateField'

added def Subalgebra.toIntermediateField

added def Subfield.toIntermediateField

added theorem mem_subalgebraEquivIntermediateField

added theorem mem_subalgebraEquivIntermediateField_symm

added def subalgebraEquivIntermediateField

added theorem toIntermediateField'_toSubalgebra

added theorem toIntermediateField_toSubalgebra

added theorem toSubalgebra_toIntermediateField'

added theorem toSubalgebra_toIntermediateField