Commit 2026-05-29 15:08 718a8532

feat(FieldTheory/Galois/IsGaloisGroup): add IsGaloisGroup.of_algEquiv and of_ringEquiv (#38902) Add two constructors for IsGaloisGroup:

• IsGaloisGroup.of_algEquiv: if G is a Galois group on B/A and e : B ≃ₐ[A] B' is G-equivariant, then G is a Galois group on B'/A.
• IsGaloisGroup.of_ringEquiv: if G is a Galois group on B/A and e : A ≃+* A' is compatible with the algebra structures, then G is a Galois group on B/A'.