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
๐Ÿ”ธ coverage
@[implicit_reducible]
instance Rat.instFloorRing :
FloorRing โ„š
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ“ coverage
theorem Rat.floor_intCast_div_natCast (n : โ„ค) (d : โ„•) :
โŒŠโ†‘n / โ†‘dโŒ‹ = n / โ†‘d
source
๐Ÿ“ coverage
theorem Rat.ceil_intCast_div_natCast (n : โ„ค) (d : โ„•) :
โŒˆโ†‘n / โ†‘dโŒ‰ = -(-n / โ†‘d)
source
๐Ÿ“ coverage
theorem Rat.floor_natCast_div_natCast (n d : โ„•) :
โŒŠโ†‘n / โ†‘dโŒ‹ = โ†‘n / โ†‘d
source
๐Ÿ“ coverage
theorem Rat.ceil_natCast_div_natCast (n d : โ„•) :
โŒˆโ†‘n / โ†‘dโŒ‰ = -(-โ†‘n / โ†‘d)
source
๐Ÿ“ coverage
theorem Rat.natFloor_natCast_div_natCast (n d : โ„•) :
โŒŠโ†‘n / โ†‘dโŒ‹โ‚Š = n / d
source
๐Ÿ“ coverage
@[simp]
theorem Rat.floor_cast {ฮฑ : Type u_1} [Field ฮฑ] [LinearOrder ฮฑ] [IsStrictOrderedRing ฮฑ] [FloorRing ฮฑ] (x : โ„š) :
โŒŠโ†‘xโŒ‹ = โŒŠxโŒ‹
source
๐Ÿ“ coverage
@[simp]
theorem Rat.ceil_cast {ฮฑ : Type u_1} [Field ฮฑ] [LinearOrder ฮฑ] [IsStrictOrderedRing ฮฑ] [FloorRing ฮฑ] (x : โ„š) :
โŒˆโ†‘xโŒ‰ = โŒˆxโŒ‰
source
๐Ÿ“ coverage
@[simp]
theorem Rat.round_cast {ฮฑ : Type u_1} [Field ฮฑ] [LinearOrder ฮฑ] [IsStrictOrderedRing ฮฑ] [FloorRing ฮฑ] (x : โ„š) :
round โ†‘x = round x
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_fract {ฮฑ : Type u_1} [Field ฮฑ] [LinearOrder ฮฑ] [IsStrictOrderedRing ฮฑ] [FloorRing ฮฑ] (x : โ„š) :
โ†‘(Int.fract x) = Int.fract โ†‘x
source
๐Ÿ“ coverage
@[simp]
theorem Rat.den_intFract (x : โ„š) :
(Int.fract x).den = x.den
source
๐Ÿ“ coverage
theorem Rat.isNat_intFloor {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„•) :
Mathlib.Meta.NormNum.IsNat r m โ†’ Mathlib.Meta.NormNum.IsNat โŒŠrโŒ‹ m
source
๐Ÿ“ coverage
theorem Rat.isInt_intFloor {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„ค) :
Mathlib.Meta.NormNum.IsInt r m โ†’ Mathlib.Meta.NormNum.IsInt โŒŠrโŒ‹ m
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
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
๐Ÿ”ธ coverage
def Rat.evalIntFloor :
Mathlib.Meta.NormNum.NormNumExt

norm_num extension for Int.floor

Instances For
    source
    ๐Ÿ“ coverage
    theorem Rat.isNat_intCeil {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„•) :
    Mathlib.Meta.NormNum.IsNat r m โ†’ Mathlib.Meta.NormNum.IsNat โŒˆrโŒ‰ m
    source
    ๐Ÿ“ coverage
    theorem Rat.isInt_intCeil {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„ค) :
    Mathlib.Meta.NormNum.IsInt r m โ†’ Mathlib.Meta.NormNum.IsInt โŒˆrโŒ‰ m
    source
    ๐Ÿ“ coverage
    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
    ๐Ÿ“ coverage
    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
    ๐Ÿ”ธ coverage
    def Rat.evalIntCeil :
    Mathlib.Meta.NormNum.NormNumExt

    norm_num extension for Int.ceil

    Instances For
      source
      ๐Ÿ“ coverage
      theorem Rat.isNat_intFract_of_isNat {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„•) :
      Mathlib.Meta.NormNum.IsNat r m โ†’ Mathlib.Meta.NormNum.IsNat (Int.fract r) 0
      source
      ๐Ÿ“ coverage
      theorem Rat.isNat_intFract_of_isInt {R : Type u_2} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„ค) :
      Mathlib.Meta.NormNum.IsInt r m โ†’ Mathlib.Meta.NormNum.IsNat (Int.fract r) 0
      source
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      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
      ๐Ÿ”ธ coverage
      def Rat.evalIntFract :
      Mathlib.Meta.NormNum.NormNumExt

      norm_num extension for Int.fract

      Instances For

        norm_num extension for round #

        source
        ๐Ÿ“ coverage
        theorem Rat.isNat_round {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„•) :
        Mathlib.Meta.NormNum.IsNat r m โ†’ Mathlib.Meta.NormNum.IsNat (round r) m
        source
        ๐Ÿ“ coverage
        theorem Rat.isInt_round {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : โ„ค) :
        Mathlib.Meta.NormNum.IsInt r m โ†’ Mathlib.Meta.NormNum.IsInt (round r) m
        source
        ๐Ÿ“ coverage
        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
        ๐Ÿ”ธ coverage
        def Rat.evalRound :
        Mathlib.Meta.NormNum.NormNumExt

        norm_num extension for round

        Instances For
          source
          ๐Ÿ“ coverage
          theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : โ„ค} {d : โ„•} :
          n % โ†‘d = n - โ†‘d * โŒŠโ†‘n / โ†‘dโŒ‹
          source
          ๐Ÿ“ coverage
          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
          ๐Ÿ“ coverage
          theorem Rat.num_lt_succ_floor_mul_den (q : โ„š) :
          q.num < (โŒŠqโŒ‹ + 1) * โ†‘q.den
          source
          ๐Ÿ“ coverage
          theorem Rat.fract_inv_num_lt_num_of_pos {q : โ„š} (q_pos : 0 < q) :
          (Int.fract qโปยน).num < q.num