data.rat.nnrat

# Nonnegative rationals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We also define an instance can_lift ℚ ℚ≥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 occurences 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.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def nnrat  :

Nonnegative rational numbers.

Equations
Instances for nnrat
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem nnrat.val_eq_coe (q : nnrat) :
q.val = q
@[protected, instance]
def nnrat.can_lift  :
(λ (q : ), 0 q)
Equations
@[ext]
theorem nnrat.ext {p q : nnrat} :
p = q p = q
@[protected]
@[simp, norm_cast]
theorem nnrat.coe_inj {p q : nnrat} :
p = q p = q
theorem nnrat.ext_iff {p q : nnrat} :
p = q p = q
theorem nnrat.ne_iff {x y : nnrat} :
x y x y
@[norm_cast]
theorem nnrat.coe_mk (q : ) (hq : 0 q) :
q, hq⟩ = q
def rat.to_nnrat (q : ) :

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

Equations
theorem rat.coe_to_nnrat (q : ) (hq : 0 q) :
theorem rat.le_coe_to_nnrat (q : ) :
@[simp]
theorem nnrat.coe_nonneg (q : nnrat) :
0 q
@[simp, norm_cast]
theorem nnrat.coe_zero  :
0 = 0
@[simp, norm_cast]
theorem nnrat.coe_one  :
1 = 1
@[simp, norm_cast]
theorem nnrat.coe_add (p q : nnrat) :
(p + q) = p + q
@[simp, norm_cast]
theorem nnrat.coe_mul (p q : nnrat) :
(p * q) = p * q
@[simp, norm_cast]
theorem nnrat.coe_inv (q : nnrat) :
@[simp, norm_cast]
theorem nnrat.coe_div (p q : nnrat) :
(p / q) = p / q
@[simp, norm_cast]
theorem nnrat.coe_bit0 (q : nnrat) :
(bit0 q) =
@[simp, norm_cast]
theorem nnrat.coe_bit1 (q : nnrat) :
(bit1 q) =
@[simp, norm_cast]
theorem nnrat.coe_sub {p 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
@[simp, norm_cast]
theorem nnrat.coe_le_coe {p q : nnrat} :
p q p q
@[simp, norm_cast]
theorem nnrat.coe_lt_coe {p q : nnrat} :
p < q p < q
@[simp, norm_cast]
theorem nnrat.coe_pos {q : nnrat} :
0 < q 0 < q
theorem nnrat.coe_mono  :
@[simp]
theorem nnrat.to_nnrat_coe (q : nnrat) :
@[simp]
@[protected]

to_nnrat and coe : ℚ≥0 → ℚ form a Galois insertion.

Equations
def nnrat.coe_hom  :

Coercion ℚ≥0 → ℚ as a ring_hom.

Equations
@[simp, norm_cast]
theorem nnrat.coe_nat_cast (n : ) :
@[simp]
theorem nnrat.mk_coe_nat (n : ) :
n, _⟩ = n
@[protected, instance]

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

Equations
@[protected, instance]
def nnrat.mul_action {α : Type u_1} [ α] :

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

Equations
@[protected, instance]
def nnrat.distrib_mul_action {α : Type u_1}  :

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

Equations
@[protected, instance]
def nnrat.module {α : Type u_1} [ α] :

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

Equations
@[simp]
theorem nnrat.coe_coe_hom  :
@[simp, norm_cast]
theorem nnrat.coe_indicator {α : Type u_1} (s : set α) (f : α nnrat) (a : α) :
(s.indicator f a) = s.indicator (λ (x : α), (f x)) a
@[simp, norm_cast]
theorem nnrat.coe_pow (q : nnrat) (n : ) :
(q ^ n) = q ^ n
@[norm_cast]
theorem nnrat.coe_list_sum (l : list nnrat) :
(l.sum) = l).sum
@[norm_cast]
theorem nnrat.coe_list_prod (l : list nnrat) :
(l.prod) = l).prod
@[norm_cast]
theorem nnrat.coe_multiset_sum (s : multiset nnrat) :
(s.sum) = s).sum
@[norm_cast]
@[norm_cast]
theorem nnrat.coe_sum {α : Type u_1} {s : finset α} {f : α nnrat} :
(s.sum (λ (a : α), f a)) = s.sum (λ (a : α), (f a))
theorem nnrat.to_nnrat_sum_of_nonneg {α : Type u_1} {s : finset α} {f : α } (hf : (a : α), a s 0 f a) :
(s.sum (λ (a : α), f a)).to_nnrat = s.sum (λ (a : α), (f a).to_nnrat)
@[norm_cast]
theorem nnrat.coe_prod {α : Type u_1} {s : finset α} {f : α nnrat} :
(s.prod (λ (a : α), f a)) = s.prod (λ (a : α), (f a))
theorem nnrat.to_nnrat_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α } (hf : (a : α), a s 0 f a) :
(s.prod (λ (a : α), f a)).to_nnrat = s.prod (λ (a : α), (f a).to_nnrat)
@[norm_cast]
theorem nnrat.nsmul_coe (q : nnrat) (n : ) :
(n q) = n q
@[simp, norm_cast]
theorem nnrat.coe_max (x y : nnrat) :
y) =
@[simp, norm_cast]
theorem nnrat.coe_min (x y : nnrat) :
y) =
theorem nnrat.sub_def (p q : nnrat) :
p - q = (p - q).to_nnrat
@[simp]
theorem nnrat.abs_coe (q : nnrat) :
@[simp]
theorem rat.to_nnrat_zero  :
@[simp]
theorem rat.to_nnrat_one  :
@[simp]
theorem rat.to_nnrat_pos {q : } :
0 < q.to_nnrat 0 < q
@[simp]
theorem rat.to_nnrat_eq_zero {q : } :
q.to_nnrat = 0 q 0
theorem rat.to_nnrat_of_nonpos {q : } :
q 0 q.to_nnrat = 0

Alias of the reverse direction of rat.to_nnrat_eq_zero.

@[simp]
theorem rat.to_nnrat_le_to_nnrat_iff {p q : } (hp : 0 p) :
q p
@[simp]
theorem rat.to_nnrat_lt_to_nnrat_iff' {p q : } :
q < p 0 < p
theorem rat.to_nnrat_lt_to_nnrat_iff {p q : } (h : 0 < p) :
q < p
theorem rat.to_nnrat_lt_to_nnrat_iff_of_nonneg {p q : } (hq : 0 q) :
q < p
@[simp]
theorem rat.to_nnrat_add {p q : } (hq : 0 q) (hp : 0 p) :
(q + p).to_nnrat =
theorem rat.to_nnrat_add_le {p q : } :
(q + p).to_nnrat
theorem rat.to_nnrat_le_iff_le_coe {q : } {p : nnrat} :
theorem rat.le_to_nnrat_iff_coe_le {p : } {q : nnrat} (hp : 0 p) :
theorem rat.le_to_nnrat_iff_coe_le' {p : } {q : nnrat} (hq : 0 < q) :
theorem rat.to_nnrat_lt_iff_lt_coe {q : } {p : nnrat} (hq : 0 q) :
q.to_nnrat < p q < p
theorem rat.lt_to_nnrat_iff_coe_lt {p : } {q : nnrat} :
q < p.to_nnrat q < p
@[simp]
theorem rat.to_nnrat_bit0 {q : } (hq : 0 q) :
@[simp]
theorem rat.to_nnrat_bit1 {q : } (hq : 0 q) :
theorem rat.to_nnrat_mul {p q : } (hp : 0 p) :
(p * q).to_nnrat =
theorem rat.to_nnrat_div {p q : } (hp : 0 p) :
(p / q).to_nnrat =
theorem rat.to_nnrat_div' {p q : } (hq : 0 q) :
(p / q).to_nnrat =
def rat.nnabs (x : ) :

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

Equations
@[simp, norm_cast]
theorem rat.coe_nnabs (x : ) :

### Numerator and denominator #

def nnrat.num (q : nnrat) :

The numerator of a nonnegative rational.

Equations
def nnrat.denom (q : nnrat) :

The denominator of a nonnegative rational.

Equations
@[simp]
@[simp]
theorem nnrat.denom_coe {q : nnrat} :
theorem nnrat.ext_num_denom {p q : nnrat} (hn : p.num = q.num) (hd : p.denom = q.denom) :
p = q
theorem nnrat.ext_num_denom_iff {p q : nnrat} :
p = q p.num = q.num p.denom = q.denom
@[simp]
theorem nnrat.num_div_denom (q : nnrat) :
(q.num) / (q.denom) = q
@[protected]
def nnrat.rec {α : nnrat Sort u_1} (h : Π (m n : ), α (m / n)) (q : nnrat) :
α q

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

Equations