Theorem IsFractionRing.lift_fieldRange_eq_of_range_eq

Modification history

2024-11-21 15:34
Mathlib/RingTheory/Localization/FractionRing.lean
feat: add `IsFractionRing.lift[AlgHom]_fieldRange[_eq_of_range_eq]` (#19286) …
Added IsFractionRing.lift_fieldRange_eq_of_range_eqView on Github →