What the reduced denominator of a fraction measures

Over a unique factorization domain R with fraction field K, Mathlib's IsFractionRing.num and IsFractionRing.den write x : K as a fraction in lowest terms. This file records what den measures: it is exactly the obstruction to x being integral, in the sense that scaling x by d : R lands in the image of R precisely when den x divides d.

Main results

• IsFractionRing.den_dvd_iff_isInteger_mul: den x ∣ d ↔ IsLocalization.IsInteger R (d * x).

The forward direction holds for any denominator; the converse is where being in lowest terms matters, and it is the reason this is an Iff rather than a one-way bound.

Mathlib's existing den API answers adjacent questions — isInteger_of_isUnit_den when the denominator is a unit, isUnit_den_iff for the converse of that, num_mul_den_eq_num_iff_eq for the defining relation — but none of them relates divisibility of den to integrality of a multiple.

The statement is in the *-form algebraMap R K d * x rather than the •-form d • x that Mathlib's isInteger_smul uses. The two are equal (Algebra.smul_def), and the choice follows the consumers: a denominator bound is applied with d a numeral, where IsInteger R (4 * x) needs no rewriting and the •-form would need algebraMap_smul at every call site.

theorem IsFractionRing.den_dvd_iff_isInteger_mul {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x : K} {d : R} : ↑(den R x) ∣ d ↔ IsLocalization.IsInteger R ((algebraMap R K) d * x)

The reduced denominator is exactly the obstruction to integrality: d * x lies in the image of R if and only if den x divides d.

The forward direction is a bound on how far x is from being integral, and holds for any d that den x divides. The converse needs the fraction to be in lowest terms: d * x = s clears to d * num x = s * den x, so den x ∣ d * num x, and num x and den x being relatively prime leaves den x ∣ d.