# 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 `Semifield` here. See `Mathlib/Algebra/Field/Rat.lean` 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 scope `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.

source
def Mathlib.LibraryNote.«specialised high priority simp lemma» :
LibraryNote

It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp` using later, more general simp lemmas. In that case, the following reasons might be arguments for the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or un`@[simp]`ed):

1. There is a significant portion of the library which needs the early lemma to be available via `simp` and which doesn't have access to the more general lemmas.
2. The more general lemmas have more complicated typeclass assumptions, causing rewrites with them to be slower.

Equations

- Mathlib.LibraryNote.«specialised high priority simp lemma» = ()

Instances For

source
instance Rat.instPosMulMono :
PosMulMono ℚ
source
instance instCommSemiringNNRat :
CommSemiring ℚ≥0
Equations

- instCommSemiringNNRat = Nonneg.commSemiring

source
instance instLinearOrderNNRat :
LinearOrder ℚ≥0
Equations

- instLinearOrderNNRat = Subtype.instLinearOrder fun (q : ℚ) => 0 ≤ q

source
instance instSubNNRat :
Sub ℚ≥0
Equations

- instSubNNRat = Nonneg.sub

source
instance instInhabitedNNRat :
Inhabited ℚ≥0
Equations

- instInhabitedNNRat = Nonneg.inhabited

source
instance NNRat.instNontrivial :
Nontrivial ℚ≥0
source
instance NNRat.instOrderBot :
OrderBot ℚ≥0
Equations

- NNRat.instOrderBot = { bot := 0, bot_le := NNRat.instOrderBot._proof_1 }

source
@[simp]
theorem NNRat.val_eq_cast (q : ℚ≥0) :
↑q = ↑q
source
instance NNRat.instCharZero :
CharZero ℚ≥0
source
instance NNRat.canLift :
CanLift ℚ ℚ≥0 NNRat.cast fun (q : ℚ) => 0 ≤ q
source
theorem NNRat.ext {p q : ℚ≥0} :
↑p = ↑q → p = q
source
theorem NNRat.ext_iff {p q : ℚ≥0} :
p = q ↔ ↑p = ↑q
source
theorem NNRat.coe_injective :
Function.Injective NNRat.cast
source
@[simp]
theorem NNRat.coe_inj {p q : ℚ≥0} :
↑p = ↑q ↔ p = q
source
theorem NNRat.ne_iff {x y : ℚ≥0} :
↑x ≠ ↑y ↔ x ≠ y
source
@[simp]
theorem NNRat.coe_mk (q : ℚ) (hq : 0 ≤ q) :
↑⟨q, hq⟩ = q
source
theorem NNRat.forall {p : ℚ≥0 → Prop} :
(∀ (q : ℚ≥0), p q) ↔ ∀ (q : ℚ) (hq : 0 ≤ q), p ⟨q, hq⟩
source
theorem NNRat.exists {p : ℚ≥0 → Prop} :
(∃ (q : ℚ≥0), p q) ↔ ∃ (q : ℚ), ∃ (hq : 0 ≤ q), p ⟨q, hq⟩
source
def Rat.toNNRat (q : ℚ) :
ℚ≥0

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

Equations

- q.toNNRat = ⟨max q 0, ⋯⟩

Instances For

source
theorem Rat.coe_toNNRat (q : ℚ) (hq : 0 ≤ q) :
↑q.toNNRat = q
source
theorem Rat.le_coe_toNNRat (q : ℚ) :
q ≤ ↑q.toNNRat
source
@[simp]
theorem NNRat.coe_nonneg (q : ℚ≥0) :
0 ≤ ↑q
source
@[simp]
theorem NNRat.coe_zero :
↑0 = 0
source
@[simp]
theorem NNRat.num_zero :
num 0 = 0
source
@[simp]
theorem NNRat.den_zero :
den 0 = 1
source
@[simp]
theorem NNRat.coe_one :
↑1 = 1
source
@[simp]
theorem NNRat.num_one :
num 1 = 1
source
@[simp]
theorem NNRat.den_one :
den 1 = 1
source
@[simp]
theorem NNRat.coe_add (p q : ℚ≥0) :
↑(p + q) = ↑p + ↑q
source
@[simp]
theorem NNRat.coe_mul (p q : ℚ≥0) :
↑(p * q) = ↑p * ↑q
source
@[simp]
theorem NNRat.coe_pow (q : ℚ≥0) (n : ℕ) :
↑(q ^ n) = ↑q ^ n
source
@[simp]
theorem NNRat.num_pow (q : ℚ≥0) (n : ℕ) :
(q ^ n).num = q.num ^ n
source
@[simp]
theorem NNRat.den_pow (q : ℚ≥0) (n : ℕ) :
(q ^ n).den = q.den ^ n
source
@[simp]
theorem NNRat.coe_sub {p q : ℚ≥0} (h : q ≤ p) :
↑(p - q) = ↑p - ↑q
source
@[simp]
theorem NNRat.coe_eq_zero {q : ℚ≥0} :
↑q = 0 ↔ q = 0
source
theorem NNRat.coe_ne_zero {q : ℚ≥0} :
↑q ≠ 0 ↔ q ≠ 0
source
@[simp]
theorem NNRat.mk_zero :
⟨0, ⋯⟩ = 0
source
theorem NNRat.coe_le_coe {p q : ℚ≥0} :
↑p ≤ ↑q ↔ p ≤ q
source
theorem NNRat.coe_lt_coe {p q : ℚ≥0} :
↑p < ↑q ↔ p < q
source
theorem NNRat.coe_pos {q : ℚ≥0} :
0 < ↑q ↔ 0 < q
source
theorem NNRat.coe_mono :
Monotone NNRat.cast
source
theorem NNRat.toNNRat_mono :
Monotone Rat.toNNRat
source
@[simp]
theorem NNRat.toNNRat_coe (q : ℚ≥0) :
(↑q).toNNRat = q
source
@[simp]
theorem NNRat.toNNRat_coe_nat (n : ℕ) :
(↑n).toNNRat = ↑n
source
def NNRat.gi :
GaloisInsertion Rat.toNNRat NNRat.cast

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

Equations

- NNRat.gi = GaloisInsertion.monotoneIntro NNRat.coe_mono NNRat.toNNRat_mono Rat.le_coe_toNNRat NNRat.toNNRat_coe

Instances For

source
def NNRat.coeHom :
ℚ≥0 →+* ℚ

Coercion `ℚ≥0 → ℚ` as a `RingHom`.

Equations

- NNRat.coeHom = { toFun := NNRat.cast, map_one' := NNRat.coe_one, map_mul' := NNRat.coe_mul, map_zero' := NNRat.coe_zero, map_add' := NNRat.coe_add }

Instances For

source
@[simp]
theorem NNRat.coe_natCast (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem NNRat.mk_natCast (n : ℕ) :
⟨↑n, ⋯⟩ = ↑n
source
@[simp]
theorem NNRat.coe_coeHom :
⇑coeHom = NNRat.cast
source
theorem NNRat.nsmul_coe (q : ℚ≥0) (n : ℕ) :
↑(n • q) = n • ↑q
source
theorem NNRat.bddAbove_coe {s : Set ℚ≥0} :
BddAbove (NNRat.cast '' s) ↔ BddAbove s
source
theorem NNRat.bddBelow_coe (s : Set ℚ≥0) :
BddBelow (NNRat.cast '' s)
source
theorem NNRat.coe_max (x y : ℚ≥0) :
↑(max x y) = max ↑x ↑y
source
theorem NNRat.coe_min (x y : ℚ≥0) :
↑(min x y) = min ↑x ↑y
source
theorem NNRat.sub_def (p q : ℚ≥0) :
p - q = (↑p - ↑q).toNNRat
source
@[simp]
theorem NNRat.abs_coe (q : ℚ≥0) :
|↑q| = ↑q
source
@[simp]
theorem NNRat.nonpos_iff_eq_zero (q : ℚ≥0) :
q ≤ 0 ↔ q = 0
source
@[simp]
theorem Rat.toNNRat_zero :
toNNRat 0 = 0
source
@[simp]
theorem Rat.toNNRat_one :
toNNRat 1 = 1
source
@[simp]
theorem Rat.toNNRat_pos {q : ℚ} :
0 < q.toNNRat ↔ 0 < q
source
@[simp]
theorem Rat.toNNRat_eq_zero {q : ℚ} :
q.toNNRat = 0 ↔ q ≤ 0
source
theorem Rat.toNNRat_of_nonpos {q : ℚ} :
q ≤ 0 → q.toNNRat = 0

Alias of the reverse direction of `Rat.toNNRat_eq_zero`.

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

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

Equations

- Rat.nnabs x = ⟨|x|, ⋯⟩

Instances For

source
@[simp]
theorem Rat.coe_nnabs (x : ℚ) :
↑(nnabs x) = |x|

### Numerator and denominator #

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

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

See also `Rat.divInt` and `mkRat`.

Equations

- NNRat.divNat n d = ⟨Rat.divInt ↑n ↑d, ⋯⟩

Instances For

source
@[simp]
theorem NNRat.coe_divNat (n d : ℕ) :
↑(divNat n d) = Rat.divInt ↑n ↑d
source
theorem NNRat.mk_divInt (n d : ℕ) :
⟨Rat.divInt ↑n ↑d, ⋯⟩ = divNat n d
source
theorem NNRat.divNat_inj {n₁ n₂ d₁ d₂ : ℕ} (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) :
divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁
source
@[simp]
theorem NNRat.divNat_zero (n : ℕ) :
divNat n 0 = 0
source
@[simp]
theorem NNRat.num_divNat_den (q : ℚ≥0) :
divNat q.num q.den = q
source
theorem NNRat.natCast_eq_divNat (n : ℕ) :
↑n = divNat n 1
source
theorem NNRat.divNat_mul_divNat (n₁ n₂ : ℕ) {d₁ d₂ : ℕ} :
divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)
source
theorem NNRat.divNat_mul_left {a : ℕ} (ha : a ≠ 0) (n d : ℕ) :
divNat (a * n) (a * d) = divNat n d
source
theorem NNRat.divNat_mul_right {a : ℕ} (ha : a ≠ 0) (n d : ℕ) :
divNat (n * a) (d * a) = divNat n d
source
@[simp]
theorem NNRat.mul_den_eq_num (q : ℚ≥0) :
q * ↑q.den = ↑q.num
source
@[simp]
theorem NNRat.den_mul_eq_num (q : ℚ≥0) :
↑q.den * q = ↑q.num
source
def NNRat.numDenCasesOn {C : ℚ≥0 → Sort u} (q : ℚ≥0) (H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (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

source
theorem NNRat.add_def (q r : ℚ≥0) :
q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)
source
theorem NNRat.mul_def (q r : ℚ≥0) :
q * r = divNat (q.num * r.num) (q.den * r.den)
source
theorem NNRat.lt_def {p q : ℚ≥0} :
p < q ↔ p.num * q.den < q.num * p.den
source
theorem NNRat.le_def {p q : ℚ≥0} :
p ≤ q ↔ p.num * q.den ≤ q.num * p.den
source
theorem Mathlib.Tactic.Qify.nnratCast_eq (a b : ℚ≥0) :
a = b ↔ ↑a = ↑b
source
theorem Mathlib.Tactic.Qify.nnratCast_le (a b : ℚ≥0) :
a ≤ b ↔ ↑a ≤ ↑b
source
theorem Mathlib.Tactic.Qify.nnratCast_lt (a b : ℚ≥0) :
a < b ↔ ↑a < ↑b
source
theorem Mathlib.Tactic.Qify.nnratCast_ne (a b : ℚ≥0) :
a ≠ b ↔ ↑a ≠ ↑b