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.ceil_def (q : ℚ) :
⌈q⌉ = -(-q.num / ↑q.den)
source
theorem Rat.floor_intCast_div_natCast (n : ℤ) (d : ℕ) :
⌊↑n / ↑d⌋ = n / ↑d
source
theorem Rat.ceil_intCast_div_natCast (n : ℤ) (d : ℕ) :
⌈↑n / ↑d⌉ = -(-n / ↑d)
source
theorem Rat.floor_natCast_div_natCast (n d : ℕ) :
⌊↑n / ↑d⌋ = ↑n / ↑d
source
theorem Rat.ceil_natCast_div_natCast (n d : ℕ) :
⌈↑n / ↑d⌉ = -(-↑n / ↑d)
source
theorem Rat.natFloor_natCast_div_natCast (n d : ℕ) :
⌊↑n / ↑d⌋₊ = n / d
source
@[deprecated Rat.floor_intCast_div_natCast]
theorem Rat.floor_int_div_nat_eq_div (n : ℤ) (d : ℕ) :
⌊↑n / ↑d⌋ = n / ↑d

Alias of Rat.floor_intCast_div_natCast.

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 Rat.isNat_intCeil {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_intCeil {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_intCeil_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.evalIntCeil :
    Mathlib.Meta.NormNum.NormNumExt

    norm_num extension for Int.ceil

    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