Commit 2026-06-20 09:31 fbfd7f57

View on Github →

refactor(RingTheory/Localization/FractionRing): remove bottom ring and field from IsFractionRing.mulSemiringAction (#40804) This PR removes the bottom ring and field from IsFractionRing.mulSemiringAction since they are unnecessary.

Estimated changes

Modified Mathlib/Algebra/Ring/Action/Group.lean

modified def MulSemiringAction.toRingEquiv

Modified Mathlib/Algebra/Star/UnitaryStarAlgAut.lean

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

deleted theorem IsGaloisGroup.toFractionRing

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

added theorem IsFractionRing.ringEquivOfRingEquivHom_apply

added theorem IsFractionRing.ringEquivOfRingEquivHom_injective

added theorem IsFractionRing.ringEquivOfRingEquiv_refl