Commit 2023-03-23 14:22 7fc680c5

View on Github →

feat: port RingTheory.Localization.NumDen (#3044)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/NumDen.lean

added theorem IsFractionRing.eq_zero_of_num_eq_zero

added theorem IsFractionRing.exists_reduced_fraction

added theorem IsFractionRing.isInteger_of_isUnit_den

added theorem IsFractionRing.isUnit_den_of_num_eq_zero

added theorem IsFractionRing.mk'_num_den'

added theorem IsFractionRing.mk'_num_den

added theorem IsFractionRing.num_den_reduced

added theorem IsFractionRing.num_mul_den_eq_num_iff_eq'

added theorem IsFractionRing.num_mul_den_eq_num_iff_eq

added theorem IsFractionRing.num_mul_den_eq_num_mul_den_iff_eq