Commit 2023-06-16 05:40 b33be3b8

View on Github →

feat: port FieldTheory.Galois (#5115)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Galois.lean

added theorem AlgEquiv.transfer_galois

added def FixedPoints.intermediateField

added theorem IntermediateField.finrank_fixedField_eq_card

added def IntermediateField.fixedField

added def IntermediateField.fixingSubgroupEquiv

added theorem IntermediateField.fixingSubgroup_fixedField

added theorem IntermediateField.le_iff_le

added theorem IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank

added theorem IsGalois.card_aut_eq_finrank

added theorem IsGalois.card_fixingSubgroup_eq_finrank

added theorem IsGalois.fixedField_fixingSubgroup

added def IsGalois.galoisCoinsertionIntermediateFieldSubgroup

added def IsGalois.galoisInsertionIntermediateFieldSubgroup

added theorem IsGalois.integral

added def IsGalois.intermediateFieldEquivSubgroup

added theorem IsGalois.is_separable_splitting_field

added theorem IsGalois.of_algEquiv

added theorem IsGalois.of_card_aut_eq_finrank

added theorem IsGalois.of_fixedField_eq_bot

added theorem IsGalois.of_separable_splitting_field

added theorem IsGalois.of_separable_splitting_field_aux

added theorem IsGalois.separable

added theorem IsGalois.splits

added theorem IsGalois.tfae

added theorem IsGalois.tower_top_of_isGalois

added theorem isGalois_iff

added theorem isGalois_iff_isGalois_bot

added theorem isGalois_iff_isGalois_top