Commit 2026-05-28 13:10 8f6faacf

View on Github →

feat(FieldTheory/Galois/IsGaloisGroup): add version of IsGaloisGroup.to_isFractionRing assuming only IsIntegral (#39091) This PR adds a version of IsGaloisGroup.to_isFractionRing assuming only Algebra.IsIntegral A B (which is weaker than the existing assumption Finite G).

Estimated changes

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

added theorem IsGaloisGroup.to_isFractionRing_of_isIntegral

Modified Mathlib/RingTheory/Invariant/Basic.lean

modified theorem IsFractionRing.isInvariant

added theorem IsFractionRing.isInvariant_of_isIntegral