Commit 2025-06-19 07:59 8a20fd89

feat(FieldTheory/Galois/IsGaloisGroup): Predicate for G being a Galois group for L/K (#26056) This PR introduces a predicate for a group G being a Galois group for an extension L/K, per this discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Galois.20Theory.20in.20mathlib The point is that L ≃ₐ[K] L is not always the most natural Galois group (e.g., B ≃ₐ[A] B might be more natural in Algebraic Number Theory, or G/H when H is a normal subgroup of G with fixed field L), so it seems reasonable to build out this more general API.