Commit 2025-10-31 23:35 f6d49f00

View on Github →

feat(FieldTheory/Galois/IsGaloisGroup): IsGaloisGroup is preserved by passing to the fraction field (#30792) This PR shows that IsGaloisGroup is preserved by passing to the fraction field.

Estimated changes

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

added theorem IsGaloisGroup.iff_isFractionRing

added theorem IsGaloisGroup.of_isFractionRing

added theorem IsGaloisGroup.to_isFractionRing