Commit 2023-03-22 13:16 3350abaf

View on Github →

feat: port RingTheory.Localization.FractionRing (#2763)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/FractionRing.lean

added theorem FractionRing.mk_eq_div

added def FractionRing

added theorem IsFractionRing.coe_inj

added theorem IsFractionRing.div_surjective

added theorem IsFractionRing.isFractionRing_iff_of_base_ringEquiv

added theorem IsFractionRing.isUnit_map_of_injective

added theorem IsFractionRing.lift_algebraMap

added theorem IsFractionRing.lift_mk'

added theorem IsFractionRing.mk'_eq_div

added theorem IsFractionRing.mk'_eq_one_iff_eq

added theorem IsFractionRing.mk'_eq_zero_iff_eq_zero

added theorem IsFractionRing.mk'_mk_eq_div

added theorem IsFractionRing.to_map_eq_zero_iff