Theorem IsGaloisGroup.toFractionRing

Modification history

2026-06-20 09:31
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
refactor(RingTheory/Localization/FractionRing): remove bottom ring and field from `IsFractionRing.mulSemiringAction` (#40804) …
Deleted IsGaloisGroup.toFractionRingView on Github →
2026-01-20 08:34
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree`, losing generality (#33873) …
Modified IsGaloisGroup.toFractionRingView on Github →
2025-11-30 13:26
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
feat(IsGaloisGroup): add `IsGaloisGroup.toFractionRing` (#32220) …
Added IsGaloisGroup.toFractionRingView on Github →