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 (a : ℚ) :

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

Equations

{num := n, denom := d, pos := h, cop := c}.floor = n / ↑d

theorem rat.le_floor {z : ℤ} {r : ℚ} :

z ≤ r.floor ↔ ↑z ≤ r

@[instance]

def rat.floor_ring :

Equations

rat.floor_ring = {floor := rat.floor, le_floor := rat.le_floor}

theorem rat.floor_def {q : ℚ} :

⌊q⌋ = q.num / ↑(q.denom)