Documentation

Mathlib.Data.Rat.Cast.Order

Casts of rational numbers into linear ordered fields. #

theorem Rat.cast_pos_of_pos {q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (hq : 0 < q) :
0 < q

Coercion from as an order embedding.

Equations
    Instances For
      @[simp]
      theorem Rat.castOrderEmbedding_apply {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (a✝ : ) :
      castOrderEmbedding a✝ = a✝
      @[simp]
      theorem Rat.cast_le {p q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      p q p q
      @[simp]
      theorem Rat.cast_lt {p q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      p < q p < q
      theorem GCongr.ratCast_le_ratCast {p q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      p qp q

      Alias of the reverse direction of Rat.cast_le.

      theorem GCongr.ratCast_lt_ratCast {p q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      p < qp < q

      Alias of the reverse direction of Rat.cast_lt.

      @[simp]
      theorem Rat.cast_nonneg {q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      0 q 0 q
      @[simp]
      theorem Rat.cast_nonpos {q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      q 0 q 0
      @[simp]
      theorem Rat.cast_pos {q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      0 < q 0 < q
      @[simp]
      theorem Rat.cast_lt_zero {q : } {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      q < 0 q < 0
      @[simp]
      theorem Rat.cast_le_natCast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m n m n
      @[simp]
      theorem Rat.natCast_le_cast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m n m n
      @[simp]
      theorem Rat.cast_le_intCast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m n m n
      @[simp]
      theorem Rat.intCast_le_cast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m n m n
      @[simp]
      theorem Rat.cast_lt_natCast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m < n m < n
      @[simp]
      theorem Rat.natCast_lt_cast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m < n m < n
      @[simp]
      theorem Rat.cast_lt_intCast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m < n m < n
      @[simp]
      theorem Rat.intCast_lt_cast {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : } :
      m < n m < n
      @[simp]
      theorem Rat.cast_min {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ) :
      (min p q) = min p q
      @[simp]
      theorem Rat.cast_max {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ) :
      (max p q) = max p q
      @[simp]
      theorem Rat.cast_abs {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ) :
      |q| = |q|
      @[simp]
      theorem Rat.preimage_cast_Icc {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ) :
      @[simp]
      theorem Rat.preimage_cast_Ico {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ) :
      @[simp]
      theorem Rat.preimage_cast_Ioc {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ) :
      @[simp]
      theorem Rat.preimage_cast_Ioo {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ) :
      @[simp]
      @[simp]

      Coercion from as an order embedding.

      Equations
        Instances For
          @[simp]
          theorem NNRat.cast_le {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p q : ℚ≥0} :
          p q p q
          @[simp]
          theorem NNRat.cast_lt {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p q : ℚ≥0} :
          p < q p < q
          @[simp]
          theorem NNRat.cast_nonpos {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :
          q 0 q 0
          @[simp]
          theorem NNRat.cast_pos {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :
          0 < q 0 < q
          theorem NNRat.cast_lt_zero {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :
          q < 0 q < 0
          @[simp]
          theorem NNRat.not_cast_lt_zero {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :
          ¬q < 0
          @[simp]
          theorem NNRat.cast_le_one {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :
          p 1 p 1
          @[simp]
          theorem NNRat.one_le_cast {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :
          1 p 1 p
          @[simp]
          theorem NNRat.cast_lt_one {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :
          p < 1 p < 1
          @[simp]
          theorem NNRat.one_lt_cast {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :
          1 < p 1 < p
          @[simp]
          @[simp]
          @[simp]
          theorem NNRat.cast_le_natCast {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ≥0} {n : } :
          m n m n
          @[simp]
          theorem NNRat.natCast_le_cast {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : ℚ≥0} :
          m n m n
          @[simp]
          theorem NNRat.cast_lt_natCast {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ≥0} {n : } :
          m < n m < n
          @[simp]
          theorem NNRat.natCast_lt_cast {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : } {n : ℚ≥0} :
          m < n m < n
          @[simp]
          theorem NNRat.cast_min {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :
          (min p q) = min p q
          @[simp]
          theorem NNRat.cast_max {K : Type u_5} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :
          (max p q) = max p q

          Extension for Rat.cast.

          Equations
            Instances For

              Extension for NNRat.cast.

              Equations
                Instances For