feat(FieldTheory/Galois): Galois group is profinite

[Thmoas-Guan]

Prove that any Galois group is profinite.

---

• depends on: [Merged by Bors] - feat(Topology/Group/Profinite): limits in the category of profinite groups #16976
• depends on: [Merged by Bors] - feat(FieldTheory/Galois): Finite galois subextensions #16978
• depends on: [Merged by Bors] - feat(FieldTheory/Galois): Lemmas of galois theory #16979
• depends on: feat(Topology/Group): continuous isomorphism #16991
• depends on: [Merged by Bors] - chore(FieldTheory/Galois): Move infinite Galois #17945
• depends on: feat(Topology/Group): Lemmas about profinite group #20282

[github-actions]

PR summary c74f39bcdf

Import changes exceeding 2%

%	File
+21.38%	Mathlib.FieldTheory.Galois.Profinite

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.FieldTheory.Galois.Profinite	1539	1868	+329 (+21.38%)

Import changes for all files

Files	Import difference
Mathlib.FieldTheory.Galois.Profinite	329

---

Declarations diff

+ AlgEquiv.aut_inv
+ ContinuousAddEquiv
+ ContinuousMulEquiv
+ ProfiniteGalGrp
+ apply_eq_iff_eq
+ apply_eq_iff_symm_apply
+ apply_symm_apply
+ bijective
+ coe_mk
+ coe_mk'
+ coe_refl
+ coe_toHomeomorph_symm
+ coe_trans
+ comp_symm_eq
+ continuousMulEquivtoLimit
+ eq_comp_symm
+ eq_symm_apply
+ eq_symm_comp
+ equivLike_inv_eq_symm
+ ext
+ finGaloisGroupFunctor_proj
+ homtoLimit
+ injective
+ instSMulMemClass
+ instance : EquivLike (M ≃ₜ* N) M N
+ instance : HomeomorphClass (M ≃ₜ* N) M N
+ instance : Inhabited (M ≃ₜ* M) := ⟨ContinuousMulEquiv.refl M⟩
+ instance : MulEquivClass (M ≃ₜ* N) M N
+ instance [IsGalois k K] : CompactSpace (K ≃ₐ[k] K)
+ instance [IsGalois k K] : T2Space (K ≃ₐ[k] K) := krullTopology_t2
+ instance [IsGalois k K] : TotallyDisconnectedSpace (K ≃ₐ[k] K)
+ instance {M N} [Unique M] [Unique N] [Mul M] [Mul N]
+ invFun_eq_symm
+ limtoGalContinuous
+ limtoGalHomeo
+ mk'
+ mk_toAlgEquivAux
+ mulEquivtoLimit
+ ofContinuousMulEquiv
+ ofUnique
+ profinGaloisGroupFunctor
+ proj
+ proj_lift
+ proj_lift_adjoin_simple
+ refl
+ refl_apply
+ restrictNormalHomContinuous
+ self_comp_symm
+ self_trans_symm
+ surjective
+ symm
+ symm_apply_apply
+ symm_apply_eq
+ symm_comp_eq
+ symm_comp_self
+ symm_symm
+ symm_trans_apply
+ symm_trans_self
+ toAlgEquiv
+ toAlgEquivAux
+ toAlgEquivAux_def
+ toAlgEquivAux_eq_liftNormal
+ toEquiv_eq_coe
+ toHomeomorph_eq_coe
+ toMulEquiv_eq_coe
+ totallyDisconnectedSpace
+ trans
+ trans_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Topology/Group/Profinite): limits in the category of profinite groups #16976
• [Merged by Bors] - feat(FieldTheory/Galois): Finite galois subextensions #16978
• [Merged by Bors] - feat(FieldTheory/Galois): Lemmas of galois theory #16979
• feat(Topology/Group): continuous isomorphism #16991
• [Merged by Bors] - chore(FieldTheory/Galois): Move infinite Galois #17945
• feat(Topology/Group): Lemmas about profinite group #20282
  By Dependent Issues (🤖). Happy coding!