Properties of integer quotients Rat.divInt

Elementary properties of Rat.divInt a b: the reduced numerator magnitude in terms of Nat.gcd a.natAbs b.natAbs, the numerator sign bit, and magnitude bounds on numerator and denominator.

Main results

• Rat.natAbs_num_divInt_of_ne_zero: numerator magnitude for b ≠ 0.
• Rat.natAbs_num_divInt: unconditional numerator magnitude.
• Rat.natAbs_num_divInt_le: numerator magnitude bound |num| ≤ |a|.
• Rat.den_divInt_le: denominator bound den ≤ |b|.
• Rat.decide_num_divInt_lt_zero_of_ne_zero: numerator sign bit for b ≠ 0.
• Rat.decide_num_divInt_lt_zero: unconditional numerator sign bit.

theorem Rat.natAbs_num_divInt_of_ne_zero (a b : ℤ) (hb : b ≠ 0) : (divInt a b).num.natAbs = a.natAbs / a.natAbs.gcd b.natAbs

Reduced numerator magnitude of Rat.divInt a b for b ≠ 0.

theorem Rat.natAbs_num_divInt (a b : ℤ) : (divInt a b).num.natAbs = if b = 0 then 0 else a.natAbs / a.natAbs.gcd b.natAbs

Reduced numerator magnitude of Rat.divInt a b for arbitrary integers a, b.

theorem Rat.natAbs_num_divInt_le (a b : ℤ) (hb : b ≠ 0) : (divInt a b).num.natAbs ≤ a.natAbs

Reduced numerator magnitude of Rat.divInt a b is bounded by |a|.

theorem Rat.den_divInt_le (a b : ℤ) (hb : b ≠ 0) : (divInt a b).den ≤ b.natAbs

Reduced denominator of Rat.divInt a b is bounded by |b|.

theorem Rat.decide_num_divInt_lt_zero_of_ne_zero (a b : ℤ) (hb : b ≠ 0) : decide ((divInt a b).num < 0) = if a = 0 then false else decide (a < 0) ^^ decide (b < 0)

Sign bit of Rat.divInt a b for b ≠ 0.

theorem Rat.decide_num_divInt_lt_zero (a b : ℤ) : decide ((divInt a b).num < 0) = if a = 0 then false else if b = 0 then false else decide (a < 0) ^^ decide (b < 0)

Sign bit of Rat.divInt a b for arbitrary integers a, b.