Theorem IsGaloisGroup.to_isFractionRing_of_isIntegral

Modification history

2026-06-23 14:13

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

chore(FieldTheory/IsGaloisGroup): split file by imports (#40942) …

Modified IsGaloisGroup.to_isFractionRing_of_isIntegral View on Github →

2026-05-28 13:10

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

feat(FieldTheory/Galois/IsGaloisGroup): add version of `IsGaloisGroup.to_isFractionRing` assuming only `IsIntegral` (#39091) …

Added IsGaloisGroup.to_isFractionRing_of_isIntegral View on Github →