# 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 : ) :
= a.num / a.den
theorem Rat.le_floor {z : } {r : } :
z 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} [] (x : ) :
@[simp]
theorem Rat.ceil_cast {α : Type u_1} [] (x : ) :
@[simp]
theorem Rat.round_cast {α : Type u_1} [] (x : ) :
round x =
@[simp]
theorem Rat.cast_fract {α : Type u_1} [] (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 (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) :
().num < q.num