mathlib documentation

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

source
@[protected, instance]
def nnrat.canonically_linear_ordered_semifield  :
canonically_linear_ordered_semifield nnrat
source
@[protected, instance]
def nnrat.linear_ordered_comm_group_with_zero  :
linear_ordered_comm_group_with_zero nnrat
source
@[protected, instance]
def nnrat.archimedean  :
archimedean nnrat
source
@[protected, instance]
def nnrat.has_sub  :
has_sub nnrat
source
@[protected, instance]
def nnrat.has_ordered_sub  :
has_ordered_sub nnrat
source
def nnrat  :
Type

Nonnegative rational numbers.

Equations
Instances for nnrat
source
@[protected, instance]
def nnrat.inhabited  :
inhabited nnrat
source
@[protected, instance]
def nnrat.densely_ordered  :
densely_ordered nnrat
source
@[protected, instance]
def nnrat.canonically_ordered_comm_semiring  :
canonically_ordered_comm_semiring nnrat
source
@[protected, instance]
def nnrat.rat.has_coe  :
has_coe nnrat ℚ
Equations
source
@[simp]
theorem nnrat.val_eq_coe (q : nnrat) :
q.val = ↑q
source
@[protected, instance]
def nnrat.can_lift  :
can_lift ℚ nnrat
Equations
source
@[ext]
theorem nnrat.ext {p q : nnrat} :
↑p = ↑q → p = q
source
@[protected]
theorem nnrat.coe_injective  :
function.injective coe
source
@[simp, norm_cast]
theorem nnrat.coe_inj {p q : nnrat} :
↑p = ↑q ↔ p = q
source
theorem nnrat.ext_iff {p q : nnrat} :
p = q ↔ ↑p = ↑q
source
theorem nnrat.ne_iff {x y : nnrat} :
↑x ≠ ↑y ↔ x ≠ y
source
@[norm_cast]
theorem nnrat.coe_mk (q : ℚ) (hq : 0 ≤ q) :
↑⟨q, hq⟩ = q
source
def rat.to_nnrat (q : ℚ) :
nnrat

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

Equations
source
theorem rat.coe_to_nnrat (q : ℚ) (hq : 0 ≤ q) :
↑(q.to_nnrat) = q
source
theorem rat.le_coe_to_nnrat (q : ℚ) :
q ≤ ↑(q.to_nnrat)
source
@[simp]
theorem nnrat.coe_nonneg (q : nnrat) :
0 ≤ ↑q
source
@[simp, norm_cast]
theorem nnrat.coe_zero  :
↑0 = 0
source
@[simp, norm_cast]
theorem nnrat.coe_one  :
↑1 = 1
source
@[simp, norm_cast]
theorem nnrat.coe_add (p q : nnrat) :
↑(p + q) = ↑p + ↑q
source
@[simp, norm_cast]
theorem nnrat.coe_mul (p q : nnrat) :
↑(p * q) = ↑p * ↑q
source
@[simp, norm_cast]
theorem nnrat.coe_inv (q : nnrat) :
↑q⁻¹ = (↑q)⁻¹
source
@[simp, norm_cast]
theorem nnrat.coe_div (p q : nnrat) :
↑(p / q) = ↑p / ↑q
source
@[simp, norm_cast]
theorem nnrat.coe_bit0 (q : nnrat) :
↑(bit0 q) = bit0 ↑q
source
@[simp, norm_cast]
theorem nnrat.coe_bit1 (q : nnrat) :
↑(bit1 q) = bit1 ↑q
source
@[simp, norm_cast]
theorem nnrat.coe_sub {p q : nnrat} (h : q ≤ p) :
↑(p - q) = ↑p - ↑q
source
@[simp]
theorem nnrat.coe_eq_zero {q : nnrat} :
↑q = 0 ↔ q = 0
source
theorem nnrat.coe_ne_zero {q : nnrat} :
↑q ≠ 0 ↔ q ≠ 0
source
@[simp, norm_cast]
theorem nnrat.coe_le_coe {p q : nnrat} :
↑p ≤ ↑q ↔ p ≤ q
source
@[simp, norm_cast]
theorem nnrat.coe_lt_coe {p q : nnrat} :
↑p < ↑q ↔ p < q
source
@[simp, norm_cast]
theorem nnrat.coe_pos {q : nnrat} :
0 < ↑q ↔ 0 < q
source
theorem nnrat.coe_mono  :
monotone coe
source
theorem nnrat.to_nnrat_mono  :
monotone rat.to_nnrat
source
@[simp]
theorem nnrat.to_nnrat_coe (q : nnrat) :
↑q.to_nnrat = q
source
@[simp]
theorem nnrat.to_nnrat_coe_nat (n : ℕ) :
↑n.to_nnrat = ↑n
source
@[protected]
def nnrat.gi  :
galois_insertion rat.to_nnrat coe

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

Equations
source
def nnrat.coe_hom  :
nnrat →+* ℚ

Coercion ℚ≥0 → ℚ as a ring_hom.

Equations
source
@[simp, norm_cast]
theorem nnrat.coe_nat_cast (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem nnrat.mk_coe_nat (n : ℕ) :
⟨↑n, _⟩ = ↑n
source
@[protected, instance]
def nnrat.rat.algebra  :
algebra nnrat ℚ

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

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

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

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

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

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

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

Equations
source
@[simp]
theorem nnrat.coe_coe_hom  :
⇑nnrat.coe_hom = coe
source
@[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
source
@[simp, norm_cast]
theorem nnrat.coe_pow (q : nnrat) (n : ℕ) :
↑(q ^ n) = ↑q ^ n
source
@[norm_cast]
theorem nnrat.coe_list_sum (l : list nnrat) :
↑(l.sum) = (list.map coe l).sum
source
@[norm_cast]
theorem nnrat.coe_list_prod (l : list nnrat) :
↑(l.prod) = (list.map coe l).prod
source
@[norm_cast]
theorem nnrat.coe_multiset_sum (s : multiset nnrat) :
↑(s.sum) = (multiset.map coe s).sum
source
@[norm_cast]
theorem nnrat.coe_multiset_prod (s : multiset nnrat) :
↑(s.prod) = (multiset.map coe s).prod
source
@[norm_cast]
theorem nnrat.coe_sum {α : Type u_1} {s : finset α} {f : α → nnrat} :
↑(s.sum (λ (a : α), f a)) = s.sum (λ (a : α), ↑(f a))
source
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)
source
@[norm_cast]
theorem nnrat.coe_prod {α : Type u_1} {s : finset α} {f : α → nnrat} :
↑(s.prod (λ (a : α), f a)) = s.prod (λ (a : α), ↑(f a))
source
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)
source
@[norm_cast]
theorem nnrat.nsmul_coe (q : nnrat) (n : ℕ) :
↑(n • q) = n • ↑q
source
theorem nnrat.bdd_above_coe {s : set nnrat} :
bdd_above (coe '' s) ↔ bdd_above s
source
theorem nnrat.bdd_below_coe (s : set nnrat) :
bdd_below (coe '' s)
source
@[simp, norm_cast]
theorem nnrat.coe_max (x y : nnrat) :
↑(linear_order.max x y) = linear_order.max ↑x ↑y
source
@[simp, norm_cast]
theorem nnrat.coe_min (x y : nnrat) :
↑(linear_order.min x y) = linear_order.min ↑x ↑y
source
theorem nnrat.sub_def (p q : nnrat) :
p - q = (↑p - ↑q).to_nnrat
source
@[simp]
theorem nnrat.abs_coe (q : nnrat) :
|↑q| = ↑q
source
@[simp]
theorem rat.to_nnrat_zero  :
0.to_nnrat = 0
source
@[simp]
theorem rat.to_nnrat_one  :
1.to_nnrat = 1
source
@[simp]
theorem rat.to_nnrat_pos {q : ℚ} :
0 < q.to_nnrat ↔ 0 < q
source
@[simp]
theorem rat.to_nnrat_eq_zero {q : ℚ} :
q.to_nnrat = 0 ↔ q ≤ 0
source
theorem rat.to_nnrat_of_nonpos {q : ℚ} :
q ≤ 0 → q.to_nnrat = 0

Alias of the reverse direction of rat.to_nnrat_eq_zero.

source
@[simp]
theorem rat.to_nnrat_le_to_nnrat_iff {p q : ℚ} (hp : 0 ≤ p) :
q.to_nnrat ≤ p.to_nnrat ↔ q ≤ p
source
@[simp]
theorem rat.to_nnrat_lt_to_nnrat_iff' {p q : ℚ} :
q.to_nnrat < p.to_nnrat ↔ q < p ∧ 0 < p
source
theorem rat.to_nnrat_lt_to_nnrat_iff {p q : ℚ} (h : 0 < p) :
q.to_nnrat < p.to_nnrat ↔ q < p
source
theorem rat.to_nnrat_lt_to_nnrat_iff_of_nonneg {p q : ℚ} (hq : 0 ≤ q) :
q.to_nnrat < p.to_nnrat ↔ q < p
source
@[simp]
theorem rat.to_nnrat_add {p q : ℚ} (hq : 0 ≤ q) (hp : 0 ≤ p) :
(q + p).to_nnrat = q.to_nnrat + p.to_nnrat
source
theorem rat.to_nnrat_add_le {p q : ℚ} :
(q + p).to_nnrat ≤ q.to_nnrat + p.to_nnrat
source
theorem rat.to_nnrat_le_iff_le_coe {q : ℚ} {p : nnrat} :
q.to_nnrat ≤ p ↔ q ≤ ↑p
source
theorem rat.le_to_nnrat_iff_coe_le {p : ℚ} {q : nnrat} (hp : 0 ≤ p) :
q ≤ p.to_nnrat ↔ ↑q ≤ p
source
theorem rat.le_to_nnrat_iff_coe_le' {p : ℚ} {q : nnrat} (hq : 0 < q) :
q ≤ p.to_nnrat ↔ ↑q ≤ p
source
theorem rat.to_nnrat_lt_iff_lt_coe {q : ℚ} {p : nnrat} (hq : 0 ≤ q) :
q.to_nnrat < p ↔ q < ↑p
source
theorem rat.lt_to_nnrat_iff_coe_lt {p : ℚ} {q : nnrat} :
q < p.to_nnrat ↔ ↑q < p
source
@[simp]
theorem rat.to_nnrat_bit0 {q : ℚ} (hq : 0 ≤ q) :
(bit0 q).to_nnrat = bit0 q.to_nnrat
source
@[simp]
theorem rat.to_nnrat_bit1 {q : ℚ} (hq : 0 ≤ q) :
(bit1 q).to_nnrat = bit1 q.to_nnrat
source
theorem rat.to_nnrat_mul {p q : ℚ} (hp : 0 ≤ p) :
(p * q).to_nnrat = p.to_nnrat * q.to_nnrat
source
theorem rat.to_nnrat_inv (q : ℚ) :
q⁻¹.to_nnrat = (q.to_nnrat)⁻¹
source
theorem rat.to_nnrat_div {p q : ℚ} (hp : 0 ≤ p) :
(p / q).to_nnrat = p.to_nnrat / q.to_nnrat
source
theorem rat.to_nnrat_div' {p q : ℚ} (hq : 0 ≤ q) :
(p / q).to_nnrat = p.to_nnrat / q.to_nnrat
source
def rat.nnabs (x : ℚ) :
nnrat

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

Equations
source
@[simp, norm_cast]
theorem rat.coe_nnabs (x : ℚ) :
↑(rat.nnabs x) = |x|

Numerator and denominator #

source
def nnrat.num (q : nnrat) :
ℕ

The numerator of a nonnegative rational.

Equations
source
def nnrat.denom (q : nnrat) :
ℕ

The denominator of a nonnegative rational.

Equations
source
@[simp]
theorem nnrat.nat_abs_num_coe {q : nnrat} :
↑q.num.nat_abs = q.num
source
@[simp]
theorem nnrat.denom_coe {q : nnrat} :
↑q.denom = q.denom
source
theorem nnrat.ext_num_denom {p q : nnrat} (hn : p.num = q.num) (hd : p.denom = q.denom) :
p = q
source
theorem nnrat.ext_num_denom_iff {p q : nnrat} :
p = q ↔ p.num = q.num ∧ p.denom = q.denom
source
@[simp]
theorem nnrat.num_div_denom (q : nnrat) :
↑(q.num) / ↑(q.denom) = q
source
@[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