mathlib documentation

data.rat.floor

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) :

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