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

@[protected]

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

@[protected]

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

z ≤ r.floor ↔ ↑z ≤ r

source

@[protected, instance]

def rat.floor_ring :

floor_ring ℚ

Equations

rat.floor_ring = floor_ring.of_floor ℚ rat.floor rat.floor_ring._proof_1

source

@[protected]

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

@[simp, norm_cast]

theorem rat.floor_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ℚ) :

⌊↑x⌋ = ⌊x⌋

source

@[simp, norm_cast]

theorem rat.ceil_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ℚ) :

⌈↑x⌉ = ⌈x⌉

source

@[simp, norm_cast]

theorem rat.round_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ℚ) :

round ↑x = round x

source

@[simp, norm_cast]

theorem rat.cast_fract {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ℚ) :

↑(int.fract x) = int.fract ↑x

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