Commit 2026-10-17 09:16 493f1f1b

View on Github →

feat(FieldTheory/Galois): intermediate fields corresponding to Sylow subgroups (#44299)

Prove existence of intermediate fields of prime power index in a Galois extension using Sylow's first theorem
Add missing versions of Sylow's first theorem and the Galois correspondence
Rename some lemmas for clarity and consistency

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

added theorem IntermediateField.le_fixedField_iff_le_fixingSubgroup

deleted theorem IntermediateField.le_iff_le

added theorem IsGalois.fixedField_le_iff_fixingSubgroup_le

Modified Mathlib/FieldTheory/Galois/Infinite.lean

Created Mathlib/FieldTheory/Galois/Sylow.lean

added theorem IsGalois.exists_intermediateField_finrank_pow_prime

added theorem IsGalois.exists_intermediateField_finrank_pow_prime_ge

added theorem IsGalois.exists_intermediateField_finrank_pow_prime_le

added theorem IsGalois.exists_intermediateField_finrank_pow_prime_le_le

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/Sylow.lean

added theorem Sylow.exists_subgroup_card_pow_prime_ge

modified theorem Sylow.exists_subgroup_card_pow_prime_le