Documentation

Mathlib.Data.NNRat.Floor

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

source
instance NNRat.instFloorSemiring :
FloorSemiring ℚ≥0
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem NNRat.floor_coe (q : ℚ≥0) :
⌊↑q⌋₊ = ⌊q⌋₊
source
@[simp]
theorem NNRat.ceil_coe (q : ℚ≥0) :
⌈↑q⌉₊ = ⌈q⌉₊
source
@[simp]
theorem NNRat.coe_floor (q : ℚ≥0) :
↑⌊q⌋₊ = ⌊↑q⌋
source
@[simp]
theorem NNRat.coe_ceil (q : ℚ≥0) :
↑⌈q⌉₊ = ⌈↑q⌉
source
theorem NNRat.floor_def (q : ℚ≥0) :
⌊q⌋₊ = q.num / q.den
source
@[simp]
theorem NNRat.floor_cast {K : Type u_1} [LinearOrderedSemifield K] [FloorSemiring K] (x : ℚ≥0) :
⌊↑x⌋₊ = ⌊x⌋₊
source
@[simp]
theorem NNRat.ceil_cast {K : Type u_1} [LinearOrderedSemifield K] [FloorSemiring K] (x : ℚ≥0) :
⌈↑x⌉₊ = ⌈x⌉₊
source
@[simp]
theorem NNRat.intFloor_cast {K : Type u_1} [LinearOrderedField K] [FloorRing K] (x : ℚ≥0) :
⌊↑x⌋ = ⌊↑x⌋
source
@[simp]
theorem NNRat.intCeil_cast {K : Type u_1} [LinearOrderedField K] [FloorRing K] (x : ℚ≥0) :
⌈↑x⌉ = ⌈↑x⌉
source
theorem NNRat.floor_natCast_div_natCast (n d : ℕ) :
⌊↑n / ↑d⌋₊ = n / d