Theorem IsGaloisGroup.toFractionRing

Modification history

2026-01-20 08:34

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …

Modified IsGaloisGroup.toFractionRing View on Github →

2025-11-30 13:26

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

feat(IsGaloisGroup): add `IsGaloisGroup.toFractionRing` (#32220) …

Added IsGaloisGroup.toFractionRing View on Github →