mathlib3 documentation

data.rat.floor

Floor Function for Rational Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : } :
@[simp, norm_cast]
theorem rat.floor_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
@[simp, norm_cast]
theorem rat.ceil_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
@[simp, norm_cast]
theorem rat.round_cast {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
@[simp, norm_cast]
theorem rat.cast_fract {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : ) :
theorem rat.fract_inv_num_lt_num_of_pos {q : } (q_pos : 0 < q) :