data.rat.floor

Floor Function for Rational Numbers #

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

@[protected]
def rat.floor  :

floor q is the largest integer z such that z ≤ q

Equations
@[protected]
theorem rat.le_floor {z : } {r : } :
@[protected, instance]
Equations
@[protected]
theorem rat.floor_def {q : } :
theorem rat.floor_int_div_nat_eq_div {n : } {d : } :
theorem rat.fract_inv_num_lt_num_of_pos {q : } (q_pos : 0 < q) :