Commit 2025-11-27 08:19 61489160

View on Github →

feat(FieldTheory/IsGaloisGroup): prove the Galois correspondence for IsGaloisGroup (#29688) This PR reproves the Galois correspondence for IsGaloisGroup.

Estimated changes

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

added theorem IsGaloisGroup.card_fixingSubgroup_eq_finrank

added theorem IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup

added theorem IsGaloisGroup.fixedPoints_bot

added theorem IsGaloisGroup.fixedPoints_fixingSubgroup

added theorem IsGaloisGroup.fixedPoints_le_of_le

added theorem IsGaloisGroup.fixedPoints_top

added theorem IsGaloisGroup.fixingSubgroup_bot

added theorem IsGaloisGroup.fixingSubgroup_fixedPoints

added theorem IsGaloisGroup.fixingSubgroup_le_of_le

added theorem IsGaloisGroup.fixingSubgroup_top

added theorem IsGaloisGroup.intermediateFieldEquivSubgroup_apply

added theorem IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply

added theorem IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual

added theorem IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup

added theorem IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup

added theorem IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply

added theorem IsGaloisGroup.of_mulEquiv_algEquiv