Documentation

Mathlib.Data.NNRat.Defs

Nonnegative rationals #

This file defines the nonnegative rationals as a subtype of Rat and provides its basic algebraic order structure.

Note that NNRat is not declared as a Field here. See Data.NNRat.Lemmas for that instance.

We also define an instance CanLift ℚ ℚ≥0. This instance can be used by the lift tactic to replace x : ℚ and hx : 0 ≤ x in the proof context with x : ℚ≥0 while replacing all occurrences of x with ↑x. This tactic also works for a function f : α → ℚ with a hypothesis hf : ∀ x, 0 ≤ f x.

Notation #

ℚ≥0 is notation for NNRat in locale NNRat.

Huge warning #

Whenever you state a lemma about the coercion ℚ≥0 → ℚ, check that Lean inserts NNRat.cast, not Subtype.val. Else your lemma will never apply.

@[simp]
theorem NNRat.val_eq_cast (q : ℚ≥0) :
q = q
instance NNRat.canLift :
CanLift ℚ≥0 NNRat.cast fun (q : ) => 0 q
Equations
theorem NNRat.ext_iff {p : ℚ≥0} {q : ℚ≥0} :
p = q p = q
theorem NNRat.ext {p : ℚ≥0} {q : ℚ≥0} :
p = qp = q
@[simp]
theorem NNRat.coe_inj {p : ℚ≥0} {q : ℚ≥0} :
p = q p = q
theorem NNRat.ne_iff {x : ℚ≥0} {y : ℚ≥0} :
x y x y
@[simp]
theorem NNRat.coe_mk (q : ) (hq : 0 q) :
q, hq = q
theorem NNRat.forall {p : ℚ≥0Prop} :
(∀ (q : ℚ≥0), p q) ∀ (q : ) (hq : 0 q), p q, hq
theorem NNRat.exists {p : ℚ≥0Prop} :
(∃ (q : ℚ≥0), p q) ∃ (q : ) (hq : 0 q), p q, hq

Reinterpret a rational number q as a non-negative rational number. Returns 0 if q ≤ 0.

Equations
  • q.toNNRat = max q 0,
Instances For
    theorem Rat.coe_toNNRat (q : ) (hq : 0 q) :
    q.toNNRat = q
    theorem Rat.le_coe_toNNRat (q : ) :
    q q.toNNRat
    @[simp]
    theorem NNRat.coe_nonneg (q : ℚ≥0) :
    0 q
    @[simp]
    theorem NNRat.coe_zero :
    0 = 0
    @[simp]
    theorem NNRat.coe_one :
    1 = 1
    @[simp]
    theorem NNRat.coe_add (p : ℚ≥0) (q : ℚ≥0) :
    (p + q) = p + q
    @[simp]
    theorem NNRat.coe_mul (p : ℚ≥0) (q : ℚ≥0) :
    (p * q) = p * q
    @[simp]
    theorem NNRat.coe_pow (q : ℚ≥0) (n : ) :
    (q ^ n) = q ^ n
    @[simp]
    theorem NNRat.num_pow (q : ℚ≥0) (n : ) :
    (q ^ n).num = q.num ^ n
    @[simp]
    theorem NNRat.den_pow (q : ℚ≥0) (n : ) :
    (q ^ n).den = q.den ^ n
    @[simp]
    theorem NNRat.coe_sub {p : ℚ≥0} {q : ℚ≥0} (h : q p) :
    (p - q) = p - q
    @[simp]
    theorem NNRat.coe_eq_zero {q : ℚ≥0} :
    q = 0 q = 0
    theorem NNRat.coe_ne_zero {q : ℚ≥0} :
    q 0 q 0
    theorem NNRat.coe_le_coe {p : ℚ≥0} {q : ℚ≥0} :
    p q p q
    theorem NNRat.coe_lt_coe {p : ℚ≥0} {q : ℚ≥0} :
    p < q p < q
    @[simp]
    theorem NNRat.coe_pos {q : ℚ≥0} :
    0 < q 0 < q
    theorem NNRat.coe_mono :
    Monotone NNRat.cast
    @[simp]
    theorem NNRat.toNNRat_coe (q : ℚ≥0) :
    (↑q).toNNRat = q
    @[simp]
    theorem NNRat.toNNRat_coe_nat (n : ) :
    (↑n).toNNRat = n

    Coercion ℚ≥0 → ℚ as a RingHom.

    Equations
    Instances For
      @[simp]
      theorem NNRat.coe_natCast (n : ) :
      n = n
      @[simp]
      theorem NNRat.mk_natCast (n : ) :
      n, = n
      @[deprecated NNRat.mk_natCast]
      theorem NNRat.mk_coe_nat (n : ) :
      n, = n

      Alias of NNRat.mk_natCast.

      @[simp]
      theorem NNRat.coe_coeHom :
      NNRat.coeHom = NNRat.cast
      theorem NNRat.nsmul_coe (q : ℚ≥0) (n : ) :
      (n q) = n q
      theorem NNRat.bddAbove_coe {s : Set ℚ≥0} :
      BddAbove (NNRat.cast '' s) BddAbove s
      theorem NNRat.bddBelow_coe (s : Set ℚ≥0) :
      BddBelow (NNRat.cast '' s)
      @[simp]
      theorem NNRat.coe_max (x : ℚ≥0) (y : ℚ≥0) :
      (max x y) = max x y
      @[simp]
      theorem NNRat.coe_min (x : ℚ≥0) (y : ℚ≥0) :
      (min x y) = min x y
      theorem NNRat.sub_def (p : ℚ≥0) (q : ℚ≥0) :
      p - q = (p - q).toNNRat
      @[simp]
      theorem NNRat.abs_coe (q : ℚ≥0) :
      |q| = q
      @[simp]
      theorem NNRat.nonpos_iff_eq_zero (q : ℚ≥0) :
      q 0 q = 0
      @[simp]
      @[simp]
      @[simp]
      theorem Rat.toNNRat_pos {q : } :
      0 < q.toNNRat 0 < q
      @[simp]
      theorem Rat.toNNRat_eq_zero {q : } :
      q.toNNRat = 0 q 0
      theorem Rat.toNNRat_of_nonpos {q : } :
      q 0q.toNNRat = 0

      Alias of the reverse direction of Rat.toNNRat_eq_zero.

      @[simp]
      theorem Rat.toNNRat_le_toNNRat_iff {p : } {q : } (hp : 0 p) :
      q.toNNRat p.toNNRat q p
      @[simp]
      theorem Rat.toNNRat_lt_toNNRat_iff' {p : } {q : } :
      q.toNNRat < p.toNNRat q < p 0 < p
      theorem Rat.toNNRat_lt_toNNRat_iff {p : } {q : } (h : 0 < p) :
      q.toNNRat < p.toNNRat q < p
      theorem Rat.toNNRat_lt_toNNRat_iff_of_nonneg {p : } {q : } (hq : 0 q) :
      q.toNNRat < p.toNNRat q < p
      @[simp]
      theorem Rat.toNNRat_add {p : } {q : } (hq : 0 q) (hp : 0 p) :
      (q + p).toNNRat = q.toNNRat + p.toNNRat
      theorem Rat.toNNRat_add_le {p : } {q : } :
      (q + p).toNNRat q.toNNRat + p.toNNRat
      theorem Rat.toNNRat_le_iff_le_coe {q : } {p : ℚ≥0} :
      q.toNNRat p q p
      theorem Rat.le_toNNRat_iff_coe_le {p : } {q : ℚ≥0} (hp : 0 p) :
      q p.toNNRat q p
      theorem Rat.le_toNNRat_iff_coe_le' {p : } {q : ℚ≥0} (hq : 0 < q) :
      q p.toNNRat q p
      theorem Rat.toNNRat_lt_iff_lt_coe {q : } {p : ℚ≥0} (hq : 0 q) :
      q.toNNRat < p q < p
      theorem Rat.lt_toNNRat_iff_coe_lt {p : } {q : ℚ≥0} :
      q < p.toNNRat q < p
      theorem Rat.toNNRat_mul {p : } {q : } (hp : 0 p) :
      (p * q).toNNRat = p.toNNRat * q.toNNRat
      def Rat.nnabs (x : ) :

      The absolute value on as a map to ℚ≥0.

      Equations
      Instances For
        @[simp]
        theorem Rat.coe_nnabs (x : ) :
        (Rat.nnabs x) = |x|

        Numerator and denominator #

        theorem NNRat.num_coe (q : ℚ≥0) :
        (↑q).num = q.num
        theorem NNRat.natAbs_num_coe {q : ℚ≥0} :
        (↑q).num.natAbs = q.num
        theorem NNRat.den_coe {q : ℚ≥0} :
        (↑q).den = q.den
        @[simp]
        theorem NNRat.num_ne_zero {q : ℚ≥0} :
        q.num 0 q 0
        @[simp]
        theorem NNRat.num_pos {q : ℚ≥0} :
        0 < q.num 0 < q
        @[simp]
        theorem NNRat.den_pos (q : ℚ≥0) :
        0 < q.den
        @[simp]
        theorem NNRat.den_ne_zero (q : ℚ≥0) :
        q.den 0
        theorem NNRat.coprime_num_den (q : ℚ≥0) :
        q.num.Coprime q.den
        @[simp]
        theorem NNRat.num_natCast (n : ) :
        (↑n).num = n
        @[simp]
        theorem NNRat.den_natCast (n : ) :
        (↑n).den = 1
        @[simp]
        theorem NNRat.num_ofNat (n : ) [n.AtLeastTwo] :
        @[simp]
        theorem NNRat.den_ofNat (n : ) [n.AtLeastTwo] :
        (OfNat.ofNat n).den = 1
        theorem NNRat.ext_num_den {p : ℚ≥0} {q : ℚ≥0} (hn : p.num = q.num) (hd : p.den = q.den) :
        p = q
        theorem NNRat.ext_num_den_iff {p : ℚ≥0} {q : ℚ≥0} :
        p = q p.num = q.num p.den = q.den
        def NNRat.divNat (n : ) (d : ) :

        Form the quotient n / d where n d : ℕ.

        See also Rat.divInt and mkRat.

        Equations
        Instances For
          @[simp]
          theorem NNRat.coe_divNat (n : ) (d : ) :
          (NNRat.divNat n d) = Rat.divInt n d
          theorem NNRat.mk_divInt (n : ) (d : ) :
          Rat.divInt n d, = NNRat.divNat n d
          theorem NNRat.divNat_inj {n₁ : } {n₂ : } {d₁ : } {d₂ : } (h₁ : d₁ 0) (h₂ : d₂ 0) :
          NNRat.divNat n₁ d₁ = NNRat.divNat n₂ d₂ n₁ * d₂ = n₂ * d₁
          @[simp]
          theorem NNRat.divNat_zero (n : ) :
          @[simp]
          theorem NNRat.num_divNat_den (q : ℚ≥0) :
          NNRat.divNat q.num q.den = q
          theorem NNRat.divNat_mul_divNat (n₁ : ) (n₂ : ) {d₁ : } {d₂ : } (hd₁ : d₁ 0) (hd₂ : d₂ 0) :
          NNRat.divNat n₁ d₁ * NNRat.divNat n₂ d₂ = NNRat.divNat (n₁ * n₂) (d₁ * d₂)
          theorem NNRat.divNat_mul_left {a : } (ha : a 0) (n : ) (d : ) :
          NNRat.divNat (a * n) (a * d) = NNRat.divNat n d
          theorem NNRat.divNat_mul_right {a : } (ha : a 0) (n : ) (d : ) :
          NNRat.divNat (n * a) (d * a) = NNRat.divNat n d
          @[simp]
          theorem NNRat.mul_den_eq_num (q : ℚ≥0) :
          q * q.den = q.num
          @[simp]
          theorem NNRat.den_mul_eq_num (q : ℚ≥0) :
          q.den * q = q.num
          def NNRat.numDenCasesOn {C : ℚ≥0Sort u} (q : ℚ≥0) (H : (n d : ) → d 0n.Coprime dC (NNRat.divNat n d)) :
          C q

          Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with nonnegative rational numbers of the form n / d with d ≠ 0 and n, d coprime.

          Equations
          • q.numDenCasesOn H = .mpr (H q.num q.den )
          Instances For
            theorem NNRat.add_def (q : ℚ≥0) (r : ℚ≥0) :
            q + r = NNRat.divNat (q.num * r.den + r.num * q.den) (q.den * r.den)
            theorem NNRat.mul_def (q : ℚ≥0) (r : ℚ≥0) :
            q * r = NNRat.divNat (q.num * r.num) (q.den * r.den)
            theorem NNRat.lt_def {p : ℚ≥0} {q : ℚ≥0} :
            p < q p.num * q.den < q.num * p.den
            theorem NNRat.le_def {p : ℚ≥0} {q : ℚ≥0} :
            p q p.num * q.den q.num * p.den