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

Rat.floor a = a.num / ↑a.den

source

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

z ≤ Rat.floor r ↔ ↑z ≤ r

source

instance Rat.instFloorRingRatInstLinearOrderedRingRat :

FloorRing ℚ

Equations

Rat.instFloorRingRatInstLinearOrderedRingRat = FloorRing.ofFloor ℚ Rat.floor Rat.instFloorRingRatInstLinearOrderedRingRat.proof_1

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 : Nat.Coprime n d) :

Nat.Coprime (Int.natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) 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