Floor Function for Rational Numbers #

Summary #

We define the floor function and the floor_ring instance on ℚ. Some technical lemmas relating floor to integer division and modulo arithmetic are derived as well as some simple inequalities.

Tags #

rat, rationals, ℚ, floor

source

def rat.floor :

ℚ → ℤ

floor q is the largest integer z such that z ≤ q

Equations

{num := n, denom := d, pos := h, cop := c}.floor = n / ↑d

source

theorem rat.le_floor {z : ℤ} {r : ℚ} :

z ≤ r.floor ↔ ↑z ≤ r

source

@[instance]

def rat.floor_ring :

floor_ring ℚ

Equations

rat.floor_ring = {floor := rat.floor, le_floor := rat.le_floor}

source

theorem rat.floor_def {q : ℚ} :

⌊q⌋ = q.num / ↑(q.denom)

source

theorem rat.floor_int_div_nat_eq_div {n : ℤ} {d : ℕ} :

⌊↑n / ↑d⌋ = n / ↑d

source

theorem int.mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} :

n % ↑d = n - (↑d) * ⌊↑n / ↑d⌋

source

theorem nat.coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.coprime d) :

(↑n - (↑d) * ⌊↑n / ↑d⌋).nat_abs.coprime d

source

theorem rat.num_lt_succ_floor_mul_denom (q : ℚ) :

q.num < (⌊q⌋ + 1) * ↑(q.denom)

source

theorem rat.fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) :

(int.fract q⁻¹).num < q.num