Documentation

Mathlib.Data.Rat.Floor

Floor Function for Rational Numbers #

Summary #

We define the FloorRing 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
theorem Rat.floor_def' (a : ℚ) :
a.floor = a.num / ↑a.den
source
theorem Rat.le_floor {z : ℤ} {r : ℚ} :
z ≤ r.floor ↔ ↑z ≤ r
source
instance Rat.instFloorRing :
FloorRing ℚ
Equations
source
theorem Rat.floor_def {q : ℚ} :
⌊q⌋ = q.num / ↑q.den
source
theorem Rat.floor_int_div_nat_eq_div {n : ℤ} {d : ℕ} :
⌊↑n / ↑d⌋ = n / ↑d
source
@[simp]
theorem Rat.floor_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ℚ) :
⌊↑x⌋ = ⌊x⌋
source
@[simp]
theorem Rat.ceil_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ℚ) :
⌈↑x⌉ = ⌈x⌉
source
@[simp]
theorem Rat.round_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ℚ) :
round ↑x = round x
source
@[simp]
theorem Rat.cast_fract {α : Type u_1} [LinearOrderedField α] [FloorRing α] (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⌋).natAbs.Coprime d
source
theorem Rat.num_lt_succ_floor_mul_den (q : ℚ) :
q.num < (⌊q⌋ + 1) * ↑q.den
source
theorem Rat.fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) :
(Int.fract q⁻¹).num < q.num