Commit 2025-02-14 13:43 611ed3cf

View on Github →

feat(FieldTheory/Galois): Galois group is profinite (#16993) Prove that any Galois group is profinite.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem AlgEquiv.aut_inv

Modified Mathlib/FieldTheory/Galois/Basic.lean

added theorem IntermediateField.fixingSubgroup_anti

Modified Mathlib/FieldTheory/Galois/GaloisClosure.lean

Modified Mathlib/FieldTheory/Galois/Profinite.lean

added theorem InfiniteGalois.algEquivToLimit_continuous

added theorem InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj

added theorem InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup

added theorem InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois

added theorem InfiniteGalois.mk_toAlgEquivAux

added theorem InfiniteGalois.mulEquivToLimit_symm_continuous

added theorem InfiniteGalois.proj_adjoin_singleton_val

added theorem InfiniteGalois.proj_of_le

added theorem InfiniteGalois.restrictNormalHom_continuous

added theorem InfiniteGalois.toAlgEquivAux_eq_liftNormal

added theorem InfiniteGalois.toAlgEquivAux_eq_proj_of_mem

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

Modified Mathlib/FieldTheory/KrullTopology.lean

deleted theorem krullTopology_mem_nhds_one

added theorem krullTopology_mem_nhds_one_iff

added theorem krullTopology_mem_nhds_one_iff_of_normal

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean