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

theorem Rat.floor_def' (a : ) :
Rat.floor a = a.num / a.den
theorem Rat.le_floor {z : } {r : } :
z Rat.floor r z r
theorem Rat.floor_def {q : } :
q = q.num / q.den
theorem Rat.floor_int_div_nat_eq_div {n : } {d : } :
n / d = n / d
@[simp]
theorem Rat.floor_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ) :
@[simp]
theorem Rat.ceil_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ) :
@[simp]
theorem Rat.round_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ) :
round x = round x
@[simp]
theorem Rat.cast_fract {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ) :
(Int.fract x) = Int.fract x
theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : } {d : } :
n % d = n - d * n / d
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
theorem Rat.num_lt_succ_floor_mul_den (q : ) :
q.num < (q + 1) * q.den
theorem Rat.fract_inv_num_lt_num_of_pos {q : } (q_pos : 0 < q) :
(Int.fract q⁻¹).num < q.num