# Documentation

Mathlib.Data.Rat.NNRat

# Nonnegative rationals #

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

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.

def NNRat :

Nonnegative rational numbers.

Instances For
Instances For
instance NNRat.canLift :
CanLift NNRat Subtype.val fun q => 0 q
theorem NNRat.ext {p : NNRat} {q : NNRat} :
p = qp = q
@[simp]
theorem NNRat.coe_inj {p : NNRat} {q : NNRat} :
p = q p = q
theorem NNRat.ext_iff {p : NNRat} {q : NNRat} :
p = q p = q
theorem NNRat.ne_iff {x : NNRat} {y : NNRat} :
x y x y
theorem NNRat.coe_mk (q : ) (hq : 0 q) :
{ val := q, property := hq } = q
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
theorem Rat.le_coe_toNNRat (q : ) :
q ↑()
@[simp]
theorem NNRat.coe_nonneg (q : NNRat) :
0 q
@[simp]
theorem NNRat.coe_zero :
0 = 0
@[simp]
theorem NNRat.coe_one :
1 = 1
@[simp]
theorem NNRat.coe_add (p : NNRat) (q : NNRat) :
↑(p + q) = p + q
@[simp]
theorem NNRat.coe_mul (p : NNRat) (q : NNRat) :
↑(p * q) = p * q
@[simp]
theorem NNRat.coe_inv (q : NNRat) :
q⁻¹ = (q)⁻¹
@[simp]
theorem NNRat.coe_div (p : NNRat) (q : NNRat) :
↑(p / q) = p / q
@[simp]
theorem NNRat.coe_sub {p : NNRat} {q : NNRat} (h : q p) :
↑(p - q) = p - q
@[simp]
theorem NNRat.coe_eq_zero {q : NNRat} :
q = 0 q = 0
theorem NNRat.coe_ne_zero {q : NNRat} :
q 0 q 0
theorem NNRat.coe_le_coe {p : NNRat} {q : NNRat} :
p q p q
theorem NNRat.coe_lt_coe {p : NNRat} {q : NNRat} :
p < q p < q
@[simp]
theorem NNRat.coe_pos {q : NNRat} :
0 < q 0 < q
theorem NNRat.coe_mono :
Monotone Subtype.val
@[simp]
theorem NNRat.toNNRat_coe (q : NNRat) :
= q
@[simp]
theorem NNRat.toNNRat_coe_nat (n : ) :
= n

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

Instances For

Coercion ℚ≥0 → ℚ as a RingHom.

Instances For
@[simp]
theorem NNRat.coe_natCast (n : ) :
n = n
@[simp]
theorem NNRat.mk_coe_nat (n : ) :
{ val := n, property := (_ : 0 n) } = n

The rational numbers are an algebra over the non-negative rationals.

A MulAction over ℚ restricts to a MulAction over ℚ≥0.

A DistribMulAction over ℚ restricts to a DistribMulAction over ℚ≥0.

A Module over ℚ restricts to a Module over ℚ≥0.

@[simp]
theorem NNRat.coe_coeHom :
= Subtype.val
@[simp]
theorem NNRat.coe_indicator {α : Type u_1} (s : Set α) (f : αNNRat) (a : α) :
↑() = Set.indicator s (fun x => ↑(f x)) a
@[simp]
theorem NNRat.coe_pow (q : NNRat) (n : ) :
↑(q ^ n) = q ^ n
theorem NNRat.coe_list_sum (l : ) :
↑() = List.sum (List.map Subtype.val l)
theorem NNRat.coe_list_prod (l : ) :
↑() = List.prod (List.map Subtype.val l)
theorem NNRat.coe_multiset_sum (s : ) :
↑() = Multiset.sum (Multiset.map Subtype.val s)
theorem NNRat.coe_multiset_prod (s : ) :
↑() = Multiset.prod (Multiset.map Subtype.val s)
theorem NNRat.coe_sum {α : Type u_1} {s : } {f : αNNRat} :
↑(Finset.sum s fun a => f a) = Finset.sum s fun a => ↑(f a)
theorem NNRat.toNNRat_sum_of_nonneg {α : Type u_1} {s : } {f : α} (hf : ∀ (a : α), a s0 f a) :
Rat.toNNRat (Finset.sum s fun a => f a) = Finset.sum s fun a => Rat.toNNRat (f a)
theorem NNRat.coe_prod {α : Type u_1} {s : } {f : αNNRat} :
↑(Finset.prod s fun a => f a) = Finset.prod s fun a => ↑(f a)
theorem NNRat.toNNRat_prod_of_nonneg {α : Type u_1} {s : } {f : α} (hf : ∀ (a : α), a s0 f a) :
Rat.toNNRat (Finset.prod s fun a => f a) = Finset.prod s fun a => Rat.toNNRat (f a)
theorem NNRat.nsmul_coe (q : NNRat) (n : ) :
↑(n q) = n q
theorem NNRat.bddAbove_coe {s : } :
BddAbove (Subtype.val '' s)
theorem NNRat.bddBelow_coe (s : ) :
BddBelow (Subtype.val '' s)
@[simp]
theorem NNRat.coe_max (x : NNRat) (y : NNRat) :
↑(max x y) = max x y
@[simp]
theorem NNRat.coe_min (x : NNRat) (y : NNRat) :
↑(min x y) = min x y
theorem NNRat.sub_def (p : NNRat) (q : NNRat) :
p - q = Rat.toNNRat (p - q)
@[simp]
theorem NNRat.abs_coe (q : NNRat) :
|q| = q
@[simp]
theorem Rat.toNNRat_zero :
= 0
@[simp]
theorem Rat.toNNRat_one :
= 1
@[simp]
theorem Rat.toNNRat_pos {q : } :
0 < 0 < q
@[simp]
theorem Rat.toNNRat_eq_zero {q : } :
= 0 q 0
theorem Rat.toNNRat_of_nonpos {q : } :
q 0 = 0

Alias of the reverse direction of Rat.toNNRat_eq_zero.

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

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

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

### Numerator and denominator #

def NNRat.num (q : NNRat) :

The numerator of a nonnegative rational.

Instances For
def NNRat.den (q : NNRat) :

The denominator of a nonnegative rational.

Instances For
@[simp]
theorem NNRat.natAbs_num_coe {q : NNRat} :
Int.natAbs (q).num =
@[simp]
theorem NNRat.den_coe {q : NNRat} :
(q).den =
theorem NNRat.ext_num_den {p : NNRat} {q : NNRat} (hn : ) (hd : ) :
p = q
theorem NNRat.ext_num_den_iff {p : NNRat} {q : NNRat} :
p = q
@[simp]
theorem NNRat.num_div_den (q : NNRat) :
↑() / ↑() = q
def NNRat.rec {α : NNRatSort u_1} (h : (m n : ) → α (m / n)) (q : NNRat) :
α q

A recursor for nonnegative rationals in terms of numerators and denominators.

Instances For