Commit 2024-12-01 09:31 81b5c5ca

View on Github →

feat(FieldTheory/Galois): Lemmas of galois theory (#16979) Add lemmas about Galois extensions, especially the special case of the Galois correspondence.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Pointwise.lean

modified theorem Subgroup.Normal.conjAct

added theorem Subgroup.Normal.of_conjugate_fixed

Modified Mathlib/FieldTheory/Galois/Basic.lean

added theorem IntermediateField.restrictNormalHom_ker

added theorem IsGalois.map_fixingSubgroup

added theorem IsGalois.normalAutEquivQuotient_apply

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

added def IntermediateField.liftAlgEquiv

added theorem IntermediateField.liftAlgEquiv_apply

Modified Mathlib/FieldTheory/Normal.lean

added theorem AlgEquiv.restrictNormalHom_apply