mathlib documentation

data.rat.floor

Floor Function for Rational Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
source
@[protected]
theorem rat.le_floor {z : ℤ} {r : ℚ} :
z ≤ r.floor ↔ ↑z ≤ r
source
@[protected, instance]
def rat.floor_ring  :
floor_ring ℚ
Equations
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