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} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (x : ℚ≥0) :
⌊↑x⌋₊ = ⌊x⌋₊
source
@[simp]
theorem NNRat.ceil_cast {K : Type u_1} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (x : ℚ≥0) :
⌈↑x⌉₊ = ⌈x⌉₊
source
@[simp]
theorem NNRat.intFloor_cast {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] (x : ℚ≥0) :
⌊↑x⌋ = ⌊↑x⌋
source
@[simp]
theorem NNRat.intCeil_cast {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] (x : ℚ≥0) :
⌈↑x⌉ = ⌈↑x⌉
source
theorem NNRat.floor_natCast_div_natCast (n d : ℕ) :
⌊↑n / ↑d⌋₊ = n / d

norm_num extension for Nat.ceil #

source
theorem Mathlib.Meta.NormNum.IsNat.natCeil {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (m : ℕ) :
IsNat r m → IsNat ⌈r⌉₊ m
source
theorem Mathlib.Meta.NormNum.IsInt.natCeil {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (m : ℕ) :
IsInt r (Int.negOfNat m) → IsNat ⌈r⌉₊ 0
source
theorem Mathlib.Meta.NormNum.IsNNRat.natCeil {R : Type u_1} [Semifield R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (n d : ℕ) (h : IsNNRat r n d) (res : ℕ) (hres : ⌈↑n / ↑d⌉₊ = res) :
IsNat ⌈r⌉₊ res
source
theorem Mathlib.Meta.NormNum.IsRat.natCeil {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (n d : ℕ) (h : IsRat r (Int.negOfNat n) d) :
IsNat ⌈r⌉₊ 0
source
def Mathlib.Meta.NormNum.evalNatCeil :
NormNumExt

norm_num extension for Nat.ceil

Instances For