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
@[instance_reducible]
instance Rat.instFloorRing :
FloorRing ℚ
Equations
source
theorem Rat.floor_def' {q : ℚ} :
⌊q⌋ = q.num / ↑q.den

This variant of floor_def uses the Int.floor (for any FloorRing) rather than Rat.floor.

source
theorem Rat.ceil_def' (q : ℚ) :
⌈q⌉ = -(-q.num / ↑q.den)

This variant of ceil_def uses the Int.ceil (for any FloorRing) rather than Rat.ceil.

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
@[simp]
theorem Rat.floor_cast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) :
⌊↑x⌋ = ⌊x⌋
source
@[simp]
theorem Rat.ceil_cast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) :
⌈↑x⌉ = ⌈x⌉
source
@[simp]
theorem Rat.round_cast {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) :
round ↑x = round x
source
@[simp]
theorem Rat.cast_fract {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : ℚ) :
↑(Int.fract x) = Int.fract ↑x
source
@[simp]
theorem Rat.den_intFract (x : ℚ) :
(Int.fract x).den = x.den
source
theorem Rat.isNat_intFloor {R : Type u_2} [Ring R] [LinearOrder 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} [Ring R] [LinearOrder R] [FloorRing R] (r : R) (m : ℤ) :
Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsInt ⌊r⌋ m
source
theorem Rat.isNat_intFloor_ofIsNNRat {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) :
Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNat ⌊r⌋ (n / d)
source
theorem Rat.isInt_intFloor_ofIsRat_neg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) :
Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsInt ⌊r⌋ (Int.negOfNat (-(-↑n / ↑d)).toNat)
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} [Ring R] [LinearOrder 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} [Ring R] [LinearOrder R] [FloorRing R] (r : R) (m : ℤ) :
    Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsInt ⌈r⌉ m
    source
    theorem Rat.isNat_intCeil_ofIsNNRat {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) :
    Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNat ⌈r⌉ (-(-↑n / ↑d)).toNat
    source
    theorem Rat.isInt_intCeil_ofIsRat_neg {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) :
    Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsInt ⌈r⌉ (Int.negOfNat (n / d))
    source
    def Rat.evalIntCeil :
    Mathlib.Meta.NormNum.NormNumExt

    norm_num extension for Int.ceil

    Instances For
      source
      theorem Rat.isNat_intFract_of_isNat {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (r : R) (m : ℕ) :
      Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat (Int.fract r) 0
      source
      theorem Rat.isNat_intFract_of_isInt {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (r : R) (m : ℤ) :
      Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsNat (Int.fract r) 0
      source
      theorem Rat.isNNRat_intFract_of_isNNRat {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) :
      Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNNRat (Int.fract r) (n % d) d
      source
      theorem Rat.isRat_intFract_of_isRat_negOfNat {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (r : α) (n d : ℕ) :
      Mathlib.Meta.NormNum.IsRat r (Int.negOfNat n) d → Mathlib.Meta.NormNum.IsRat (Int.fract r) (-↑n % ↑d) d
      source
      def Rat.evalIntFract :
      Mathlib.Meta.NormNum.NormNumExt

      norm_num extension for Int.fract

      Instances For

        norm_num extension for round #

        source
        theorem Rat.isNat_round {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (r : R) (m : ℕ) :
        Mathlib.Meta.NormNum.IsNat r m → Mathlib.Meta.NormNum.IsNat (round r) m
        source
        theorem Rat.isInt_round {R : Type u_2} [Ring R] [LinearOrder R] [FloorRing R] (r : R) (m : ℤ) :
        Mathlib.Meta.NormNum.IsInt r m → Mathlib.Meta.NormNum.IsInt (round r) m
        source
        theorem Rat.IsRat.isInt_round {R : Type u_3} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (n : ℤ) (d : ℕ) (res : ℤ) (hres : round (↑n / ↑d) = res) :
        Mathlib.Meta.NormNum.IsRat r n d → Mathlib.Meta.NormNum.IsInt (round r) res
        source
        def Rat.evalRound :
        Mathlib.Meta.NormNum.NormNumExt

        norm_num extension for round

        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