Floor Function for Non-negative Rational Numbers

Summary

We define the FloorSemiring instance on ℚ≥0, and relate its operators to NNRat.cast.

Note that we cannot talk about Int.fract, which currently only works for rings.

Tags

nnrat, rationals, ℚ≥0, floor

instance NNRat.instFloorSemiring : FloorSemiring ℚ≥0

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NNRat.floor_coe (q : ℚ≥0) : ⌊↑q⌋₊ = ⌊q⌋₊

@[simp]

theorem NNRat.ceil_coe (q : ℚ≥0) : ⌈↑q⌉₊ = ⌈q⌉₊

@[simp]

theorem NNRat.coe_floor (q : ℚ≥0) : ↑⌊q⌋₊ = ⌊↑q⌋

@[simp]

theorem NNRat.coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈↑q⌉

theorem NNRat.floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den

@[simp]

theorem NNRat.floor_cast {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (x : ℚ≥0) : ⌊↑x⌋₊ = ⌊x⌋₊

@[simp]

theorem NNRat.ceil_cast {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (x : ℚ≥0) : ⌈↑x⌉₊ = ⌈x⌉₊

@[simp]

theorem NNRat.intFloor_cast {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] (x : ℚ≥0) : ⌊↑x⌋ = ⌊↑x⌋

@[simp]

theorem NNRat.intCeil_cast {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] (x : ℚ≥0) : ⌈↑x⌉ = ⌈↑x⌉

theorem NNRat.floor_natCast_div_natCast (n d : ℕ) : ⌊↑n / ↑d⌋₊ = n / d