Commit 2026-05-08 14:51 a881155c

feat(RingTheory/Localization, FieldTheory/Galois): refactor fraction field action API and add fixingSubgroup lemmas (#38377) Extracts the components of the proof of IsGaloisGroup.to_isFractionRing, adding API for working with "Galois extensions of domains". Also adds fixingSubgroup_range_algebraMap and its ring-domain analogue: if G is a Galois group for L/K and a subgroup H is a Galois group for L/R, then the elements of G fixing the range of algebraMap R L pointwise are exactly the elements of H.