Commit 2026-08-25 11:58 9817a703

feat(FieldTheory/Galois/IsGaloisGroup): generalize IsGaloisGroup.of_isScalarTower to towers of domains (#40866) Generalizes IsGaloisGroup.of_isScalarTower from a tower of fields to a tower of commutative domains: if G is a finite Galois group for B / R and R ⊆ A ⊆ B is a tower of commutative domains with A integrally closed, then the fixing subgroup of the image of A in B is a Galois group for B / A.