Quotients of integers in a field

Candidates for Mathlib.Algebra.Order.Field.Basic: in a linearly ordered field the quotient of two integers is at most the numerator in absolute value (abs_intCast_div_intCast_le_abs), also for the denominator 0, by which the quotient is 0; the field form of Int.abs_ediv_le_abs. An integer a with a / b above or below n / q lies above the quotient of b n by q rounded up, or below it rounded down (Int.neg_ediv_neg_le_of_div_le, Int.le_ediv_of_div_le). A fraction keeps its value when numerator and denominator are divided by their greatest common divisor (intCast_ediv_gcd_div_natCast_div_gcd), and the dyadic m 2 ^ e is the fraction of m 2 ^ max e 0 and 2 ^ max (-e) 0 (intCast_mul_two_pow_div_two_pow).

Main statements

• abs_intCast_div_intCast_le_abs: |x / z| ≤ |x| for integers x and z, and abs_intCast_div_natCast_le the bound by H that follows from |x| ≤ H.
• Int.le_ediv_of_div_le, Int.neg_ediv_neg_le_of_div_le: the bounds of a from a / b.

theorem abs_intCast_div_intCast_le_abs {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (x z : ℤ) : |↑x / ↑z| ≤ |↑x|

theorem abs_intCast_div_natCast_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : ℤ} {H : ℕ} (ha : |a| ≤ ↑H) (b : ℕ) : |↑a / ↑b| ≤ ↑H

theorem Int.le_ediv_of_div_le {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {n a : ℤ} {q b : ℕ} (hb : 0 < b) (h : ↑a / ↑b ≤ ↑n / ↑q) : a ≤ ↑b * n / ↑q

a ≤ ⌊b n / q⌋ for an integer a with a / b ≤ n / q, the floor written as the integer division b n / q; also for q = 0, by which both quotients are 0.

theorem Int.neg_ediv_neg_le_of_div_le {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {n a : ℤ} {q b : ℕ} (hb : 0 < b) (h : ↑n / ↑q ≤ ↑a / ↑b) : -(-(↑b * n) / ↑q) ≤ a

⌈b n / q⌉ ≤ a for an integer a with n / q ≤ a / b, the ceiling written as -(-(b n) / q) (Int.le_ediv_of_div_le for -a and -n).

theorem intCast_ediv_gcd_div_natCast_div_gcd {K : Type u_1} [DivisionRing K] [CharZero K] (n : ℤ) (q : ℕ) : ↑(n / ↑(n.natAbs.gcd q)) / ↑(q / n.natAbs.gcd q) = ↑n / ↑q

Dividing the numerator n and the denominator q of a fraction by their greatest common divisor does not change its value, also for q = 0.

theorem intCast_mul_two_pow_div_two_pow {K : Type u_1} [DivisionRing K] (m e : ℤ) : ↑(m * 2 ^ e.toNat) / ↑(2 ^ (-e).toNat) = ↑m * 2 ^ e