Theorem IsFractionRing.ringEquivOfRingEquivHom_injective

Modification history

2026-06-20 09:31
Mathlib/RingTheory/Localization/FractionRing.lean
refactor(RingTheory/Localization/FractionRing): remove bottom ring and field from `IsFractionRing.mulSemiringAction` (#40804) …
Added IsFractionRing.ringEquivOfRingEquivHom_injectiveView on Github →