feat(FieldTheory/Galois): Lemmas of galois theory

[Thmoas-Guan]

Add lemmas about Galois extensions, especially the special case of the Galois correspondence.
Co-authored-by: Yongle Hu [email protected] Nailin Guan [email protected] Jingting Wang [email protected]

---

• depends on: [Merged by Bors] - chore(FieldTheory/Galois): move file Galois into folder Galois #17197

[github-actions]

PR summary dac416d611

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ AlgEquiv.restrictNormalHom_apply
+ AlgEquiv.restrictNormalHom_ker
+ Normal.of_conjugate_fixed
+ fixingSubgroup_conjugate_of_map
+ fixingSubgroup_normal_of_isGalois
+ lift_algEquiv
+ normalAutEquivQuotient
+ normalAutEquivQuotient_apply
+ of_fixedField_normal_subgroup

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(FieldTheory/Galois): move file Galois into folder Galois #17197
  By Dependent Issues (🤖). Happy coding!

[Thmoas-Guan]

This is all the lemmas needed for the incoming PRs #16982 and #16993 , but some is still needed in #16978, do I need to remove the overlaping part or work on this PR first?

[faenuccio]

This is all the lemmas needed for the incoming PRs #16982 and #16993 , but some is still needed in #16978, do I need to remove the overlaping part or work on this PR first?

Do you mean that #16978 depends on this PR? If this is the case, please mark it there and add the blocked-by-other-PR label (add it also to the other two PR's that depend on this one).

[Thmoas-Guan]

#16978 can be handled seperately, but should I remove the overlaping part? Because some lemmas in this PR is also used in #16979, I think I should just remove them for now.

[faenuccio]

#16978 can be handled seperately, but should I remove the overlaping part? Because some lemmas in this PR is also used in #16979

Well, if nothing in #16978 needs what is in this PR, then yes, you should remove the overlap: once this PR will be merged the results will be in master and there will be no need to re-add them through #16978. Even better, as soon as this one is merged, when you will update master on #16978, this will import these new lemmas there, so there will be no need to add them manually. All in all, a certain def/lemma should appear in a PR only if

1. You are trying to add it to master
2. You need it for the other results of that PR.