Ring-theoretic fractions in ℚ

theorem Rat.isLocalizationIsInteger_iff (q : ℚ) : IsLocalization.IsInteger ℤ q ↔ q ∈ Set.range Int.cast

theorem Rat.associated_num_den (q : ℚ) : Associated (IsFractionRing.num ℤ q) q.num ∧ Associated ↑(IsFractionRing.den ℤ q) ↑q.den

theorem Rat.isFractionRingDen (q : ℚ) : (↑(IsFractionRing.den ℤ q)).natAbs = q.den

theorem Rat.isFractionRingNum (q : ℚ) : Associated (IsFractionRing.num ℤ q) q.num