Documentation

Mathlib.Data.Rat.Floor

Floor Function for Rational Numbers #

Summary #

We define the FloorRing instance on ℚ. Some technical lemmas relating floor to integer division and modulo arithmetic are derived as well as some simple inequalities.

Tags #

rat, rationals, ℚ, floor

source
theorem Rat.floor_def' (a : ℚ) :
a.floor = a.num / ↑a.den
source
theorem Rat.le_floor {z : ℤ} {r : ℚ} :
z ≤ r.floor ↔ ↑z ≤ r
source
instance Rat.instFloorRing :
FloorRing ℚ
Equations
source
theorem Rat.floor_def {q : ℚ} :
⌊q⌋ = q.num / ↑q.den
source
theorem Rat.floor_int_div_nat_eq_div (n : ℤ) (d : ℕ) :
⌊↑n / ↑d⌋ = n / ↑d
source
@[simp]
theorem Rat.floor_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ℚ) :
⌊↑x⌋ = ⌊x⌋
source
@[simp]
theorem Rat.ceil_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ℚ) :
⌈↑x⌉ = ⌈x⌉
source
@[simp]
theorem Rat.round_cast {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ℚ) :
round ↑x = round x
source
@[simp]
theorem Rat.cast_fract {α : Type u_1} [LinearOrderedField α] [FloorRing α] (x : ℚ) :
↑(Int.fract x) = Int.fract ↑x
source
theorem Rat.isNat_intFloor {R : Type u_2} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℕ) :
Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat ⌊r⌋ m
source
theorem Rat.isInt_intFloor {R : Type u_2} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℤ) :
Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsInt ⌊r⌋ m
source
theorem Rat.isInt_intFloor_ofIsRat {α : Type u_1} [LinearOrderedField α] [FloorRing α] (r : α) (n : ℤ) (d : ℕ) :
Mathlib.Meta.NormNum.IsRat r n d → Mathlib.Meta.NormNum.IsInt ⌊r⌋ (n / ↑d)
source
def Rat.evalIntFloor :
Mathlib.Meta.NormNum.NormNumExt

norm_num extension for Int.floor

Instances For
    source
    theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} :
    n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
    source
    theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime {n : ℕ} {d : ℕ} (n_coprime_d : n.Coprime d) :
    (↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d
    source
    theorem Rat.num_lt_succ_floor_mul_den (q : ℚ) :
    q.num < (⌊q⌋ + 1) * ↑q.den
    source
    theorem Rat.fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) :
    (Int.fract q⁻¹).num < q.num