Floor Function for Rational Numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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.
rat, rationals, ℚ, floor
floor q is the largest integer
z such that
z ≤ q