mathlib documentation

data.rat.floor

Floor Function for Rational Numbers

Summary

We define the floor function and the floor_ring instance on .

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 : } :

theorem rat.floor_def {q : } :