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.

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» = ()

instance Rat.instZeroLEOneClass : ZeroLEOneClass ℚ

instance Rat.instPosMulMono : PosMulMono ℚ

instance instCommSemiringNNRat : CommSemiring ℚ≥0

Equations

• instCommSemiringNNRat = Nonneg.commSemiring

instance instLinearOrderNNRat : LinearOrder ℚ≥0

Equations

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

instance instSubNNRat : Sub ℚ≥0

Equations

• instSubNNRat = Nonneg.sub

instance instInhabitedNNRat : Inhabited ℚ≥0

Equations

• instInhabitedNNRat = Nonneg.inhabited

instance NNRat.instNontrivial : Nontrivial ℚ≥0

instance NNRat.instOrderBot : OrderBot ℚ≥0

Equations

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

@[simp]

theorem NNRat.val_eq_cast (q : ℚ≥0) : ↑q = ↑q

instance NNRat.instCharZero : CharZero ℚ≥0

instance NNRat.canLift : CanLift ℚ ℚ≥0 NNRat.cast fun (q : ℚ) => 0 ≤ q

theorem NNRat.ext {p q : ℚ≥0} : ↑p = ↑q → p = q

theorem NNRat.ext_iff {p q : ℚ≥0} : p = q ↔ ↑p = ↑q

theorem NNRat.coe_injective : Function.Injective NNRat.cast

@[simp]

theorem NNRat.coe_inj {p q : ℚ≥0} : ↑p = ↑q ↔ p = q

theorem NNRat.ne_iff {x y : ℚ≥0} : ↑x ≠ ↑y ↔ x ≠ y

@[simp]

theorem NNRat.coe_mk (q : ℚ) (hq : 0 ≤ q) : ↑⟨q, hq⟩ = q

theorem NNRat.forall {p : ℚ≥0 → Prop} : (∀ (q : ℚ≥0), p q) ↔ ∀ (q : ℚ) (hq : 0 ≤ q), p ⟨q, hq⟩

theorem NNRat.exists {p : ℚ≥0 → Prop} : (∃ (q : ℚ≥0), p q) ↔ ∃ (q : ℚ), ∃ (hq : 0 ≤ q), p ⟨q, hq⟩

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, ⋯⟩

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.num_zero : num 0 = 0

@[simp]

theorem NNRat.den_zero : den 0 = 1

@[simp]

theorem NNRat.coe_one : ↑1 = 1

@[simp]

theorem NNRat.num_one : num 1 = 1

@[simp]

theorem NNRat.den_one : den 1 = 1

@[simp]

theorem NNRat.coe_add (p q : ℚ≥0) : ↑(p + q) = ↑p + ↑q

@[simp]

theorem NNRat.coe_mul (p 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 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

@[simp]

theorem NNRat.mk_zero : ⟨0, ⋯⟩ = 0

theorem NNRat.coe_le_coe {p q : ℚ≥0} : ↑p ≤ ↑q ↔ p ≤ q

theorem NNRat.coe_lt_coe {p q : ℚ≥0} : ↑p < ↑q ↔ p < q

theorem NNRat.coe_pos {q : ℚ≥0} : 0 < ↑q ↔ 0 < q

theorem NNRat.coe_mono : Monotone NNRat.cast

theorem NNRat.toNNRat_mono : Monotone Rat.toNNRat

@[simp]

theorem NNRat.toNNRat_coe (q : ℚ≥0) : (↑q).toNNRat = q

@[simp]

theorem NNRat.toNNRat_coe_nat (n : ℕ) : (↑n).toNNRat = ↑n

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

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 }

@[simp]

theorem NNRat.coe_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem NNRat.mk_natCast (n : ℕ) : ⟨↑n, ⋯⟩ = ↑n

@[simp]

theorem NNRat.coe_coeHom : ⇑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)

theorem NNRat.coe_max (x y : ℚ≥0) : ↑(max x y) = max ↑x ↑y

theorem NNRat.coe_min (x y : ℚ≥0) : ↑(min x y) = min ↑x ↑y

theorem NNRat.sub_def (p 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 : toNNRat 0 = 0

@[simp]

theorem Rat.toNNRat_one : toNNRat 1 = 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 ≤ 0 → q.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 : ℚ) : ℚ≥0

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

Equations

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

@[simp]

theorem Rat.coe_nnabs (x : ℚ) : ↑(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 = OfNat.ofNat n

@[simp]

theorem NNRat.den_ofNat (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).den = 1

theorem NNRat.ext_num_den {p q : ℚ≥0} (hn : p.num = q.num) (hd : p.den = q.den) : p = q

theorem NNRat.ext_num_den_iff {p q : ℚ≥0} : p = q ↔ p.num = q.num ∧ p.den = q.den

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, ⋯⟩

@[simp]

theorem NNRat.coe_divNat (n d : ℕ) : ↑(divNat n d) = Rat.divInt ↑n ↑d

theorem NNRat.mk_divInt (n d : ℕ) : ⟨Rat.divInt ↑n ↑d, ⋯⟩ = divNat n d

theorem NNRat.divNat_inj {n₁ n₂ d₁ d₂ : ℕ} (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

@[simp]

theorem NNRat.divNat_zero (n : ℕ) : divNat n 0 = 0

@[simp]

theorem NNRat.num_divNat_den (q : ℚ≥0) : divNat q.num q.den = q

theorem NNRat.natCast_eq_divNat (n : ℕ) : ↑n = divNat n 1

theorem NNRat.divNat_mul_divNat (n₁ n₂ : ℕ) {d₁ d₂ : ℕ} : divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

theorem NNRat.divNat_mul_left {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (a * n) (a * d) = divNat n d

theorem NNRat.divNat_mul_right {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (n * a) (d * a) = 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 : ℚ≥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 ⋯ ⋯)

theorem NNRat.add_def (q r : ℚ≥0) : q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)

theorem NNRat.mul_def (q r : ℚ≥0) : q * r = divNat (q.num * r.num) (q.den * r.den)

theorem NNRat.lt_def {p q : ℚ≥0} : p < q ↔ p.num * q.den < q.num * p.den

theorem NNRat.le_def {p q : ℚ≥0} : p ≤ q ↔ p.num * q.den ≤ q.num * p.den

theorem Mathlib.Tactic.Qify.nnratCast_eq (a b : ℚ≥0) : a = b ↔ ↑a = ↑b

theorem Mathlib.Tactic.Qify.nnratCast_le (a b : ℚ≥0) : a ≤ b ↔ ↑a ≤ ↑b

theorem Mathlib.Tactic.Qify.nnratCast_lt (a b : ℚ≥0) : a < b ↔ ↑a < ↑b

theorem Mathlib.Tactic.Qify.nnratCast_ne (a b : ℚ≥0) : a ≠ b ↔ ↑a ≠ ↑b