# 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.

Equations
Equations
@[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 : } :
(∀ (q : ℚ≥0), p q) ∀ (q : ) (hq : 0 q), p q, hq
theorem NNRat.exists {p : } :
(∃ (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

toNNRat and (↑) : ℚ≥0 → ℚ form a Galois insertion.

Equations
Instances For

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.cast
theorem NNRat.nsmul_coe (q : ℚ≥0) (n : ) :
(n q) = n q
theorem NNRat.bddAbove_coe {s : } :
BddAbove (NNRat.cast '' s)
theorem NNRat.bddBelow_coe (s : ) :
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]
theorem Rat.toNNRat_zero :
= 0
@[simp]
theorem Rat.toNNRat_one :
= 1
@[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
• = |x|,
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] :
(OfNat.ofNat n).num =
@[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, =
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 : ) :
= 0
@[simp]
theorem NNRat.num_divNat_den (q : ℚ≥0) :
NNRat.divNat q.num q.den = q
theorem NNRat.natCast_eq_divNat (n : ) :
n =
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) =
theorem NNRat.divNat_mul_right {a : } (ha : a 0) (n : ) (d : ) :
NNRat.divNat (n * a) (d * a) =
@[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