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 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 LibraryNote.specialised_high_priority_simp_lemma :

Batteries.Util.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):

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.
The more general lemmas have more complicated typeclass assumptions, causing rewrites with them to be slower.

Instances For

instance Rat.instPosMulMono :

@[implicit_reducible]

instance instCommSemiringNNRat :

CommSemiring ℚ≥0

@[implicit_reducible]

instance instAddCancelCommMonoidNNRat :

AddCancelCommMonoid ℚ≥0

@[implicit_reducible]

instance instLinearOrderNNRat :

LinearOrder ℚ≥0

@[implicit_reducible]

instance instSubNNRat :

@[implicit_reducible]

instance instInhabitedNNRat :

Inhabited ℚ≥0

instance NNRat.instNontrivial :

Nontrivial ℚ≥0

@[implicit_reducible]

instance NNRat.instOrderBot :

OrderBot ℚ≥0

@[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 : ℚ) :

Reinterpret a rational number q as a non-negative rational number. Returns 0 if 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.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

GaloisInsertion Rat.toNNRat NNRat.cast

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

Instances For

def NNRat.coeHom :

ℚ≥0 →+* ℚ

Coercion ℚ≥0 → ℚ as a RingHom.

Instances For

@[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 :

@[simp]

theorem Rat.toNNRat_one :

@[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 : ℚ) :

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

Instances For

@[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 : ℕ) :

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

See also Rat.divInt and mkRat.

Instances For

@[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.

Instances For

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