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
@[instance]
Equations
- rat.floor_ring = {floor := rat.floor, le_floor := rat.le_floor}