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

def rat.floor  :

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

Equations
theorem rat.le_floor {z : } {r : } :
@[instance]
Equations
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) :