Commit 2026-03-17 12:17 60d70699

feat(FieldTheory/Galois/IsGaloisGroup): Galois groups for quotients by normal subgroups (#36391) Assume G is a finite Galois group for L/K, N ⊴ G is normal, and F = Fix(N). This PR proves:

• G ⧸ N acts on F via (g.N) • x := g • x as a MulSemiringAction. Under SMulCommClass G K L, it is also SMulCommClass (G ⧸ N) K F
• instance quotient : IsGaloisGroup (G ⧸ N) K F — the quotient group is a Galois group for the intermediate extension F/K.
• theorem quotientMap under the hypothesis E ≤ F: IsGaloisGroup (H.map (QuotientGroup.mk' N)) E F — if H is the Galois group for L/E, the image of H under the quotient map is a Galois group for F/E.