Mathlib.Data.NNRat.Defs

Rat.instZeroLEOneClass instance

: ZeroLEOneClass ℚ

Full source

instance Rat.instZeroLEOneClass : ZeroLEOneClass ℚ where
  zero_le_one := rfl

Nonnegativity of Zero and One in Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ satisfy the inequality $0 \leq 1$ with respect to their natural order.

Rat.instPosMulMono instance

: PosMulMono ℚ

Full source

instance Rat.instPosMulMono : PosMulMono ℚ where
  elim := fun r p q h => by
    simp only [mul_comm]
    simpa [sub_mul, sub_nonneg] using Rat.mul_nonneg (sub_nonneg.2 h) r.2

Monotonicity of Left Multiplication by Nonnegative Rationals

Informal description

For any nonnegative rational number $b$ and any rational numbers $a_1 \leq a_2$, we have $b \cdot a_1 \leq b \cdot a_2$.

NNRat.instNontrivial instance

: Nontrivial ℚ≥0

Full source

instance instNontrivial : Nontrivial ℚ≥0 where exists_pair_ne := ⟨1, 0, by decide⟩

Nontriviality of Nonnegative Rational Numbers

Informal description

The type of nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ is nontrivial, meaning it contains at least two distinct elements.

NNRat.instOrderBot instance

: OrderBot ℚ≥0

Full source

instance instOrderBot : OrderBot ℚ≥0 where
  bot := 0
  bot_le q := q.2

Nonnegative Rationals as an Ordered Set with Bottom Element

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ form an ordered set with a bottom element $0$.

NNRat.val_eq_cast theorem

(q : ℚ≥0) : q.1 = q

Full source

@[simp] lemma val_eq_cast (q : ℚ≥0) : q.1 = q := rfl

Subtype Value Equals Canonical Embedding for Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the underlying rational number (via the subtype value) is equal to the canonical embedding of $q$ into $\mathbb{Q}$.

NNRat.instCharZero instance

: CharZero ℚ≥0

Full source

instance instCharZero : CharZero ℚ≥0 where
  cast_injective a b hab := by simpa using congr_arg num hab

Characteristic Zero Property of Nonnegative Rationals

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ form a characteristic zero monoid. That is, the canonical map from the natural numbers $\mathbb{N}$ to $\mathbb{Q}_{\geq 0}$ is injective.

NNRat.canLift instance

: CanLift ℚ ℚ≥0 (↑) fun q ↦ 0 ≤ q

Full source

instance canLift : CanLift ℚ ℚ≥0 (↑) fun q ↦ 0 ≤ q where
  prf q hq := ⟨⟨q, hq⟩, rfl⟩

Lifting Condition from Rationals to Nonnegative Rationals

Informal description

There exists a lifting condition from the rational numbers $\mathbb{Q}$ to the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ via the canonical embedding, where a rational number $q$ can be lifted if and only if $0 \leq q$.

NNRat.ext theorem

: (p : ℚ) = (q : ℚ) → p = q

Full source

@[ext]
theorem ext : (p : ℚ) = (q : ℚ) → p = q :=
  Subtype.ext

Equality of Nonnegative Rationals via Canonical Embedding

Informal description

For any two nonnegative rational numbers $p$ and $q$, if their images under the canonical embedding into $\mathbb{Q}$ are equal, then $p = q$.

NNRat.coe_injective theorem

: Injective ((↑) : ℚ≥0 → ℚ)

Full source

protected theorem coe_injective : Injective ((↑) : ℚ≥0 → ℚ) :=
  Subtype.coe_injective

Injectivity of the Canonical Embedding from Nonnegative Rationals to Rationals

Informal description

The canonical embedding from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to the rational numbers $\mathbb{Q}$ is injective. That is, for any $x, y \in \mathbb{Q}_{\geq 0}$, if $x = y$ as rational numbers, then $x = y$ as nonnegative rational numbers.

NNRat.coe_inj theorem

: (p : ℚ) = q ↔ p = q

Full source

@[simp high, norm_cast]
theorem coe_inj : (p : ℚ) = q ↔ p = q :=
  Subtype.coe_inj

Injectivity of the Canonical Embedding from Nonnegative Rationals to Rationals

Informal description

For any two nonnegative rational numbers $p$ and $q$, the canonical embedding into $\mathbb{Q}$ satisfies $(p : \mathbb{Q}) = (q : \mathbb{Q})$ if and only if $p = q$.

NNRat.ne_iff theorem

{x y : ℚ≥0} : (x : ℚ) ≠ (y : ℚ) ↔ x ≠ y

Full source

theorem ne_iff {x y : ℚ≥0} : (x : ℚ) ≠ (y : ℚ)(x : ℚ) ≠ (y : ℚ) ↔ x ≠ y :=
  NNRat.coe_inj.not

Inequality Preservation under Canonical Embedding of Nonnegative Rationals

Informal description

For any two nonnegative rational numbers $x$ and $y$, the inequality $(x : \mathbb{Q}) \neq (y : \mathbb{Q})$ holds if and only if $x \neq y$.

NNRat.coe_mk theorem

(q : ℚ) (hq) : NNRat.cast ⟨q, hq⟩ = q

Full source

@[simp, norm_cast] lemma coe_mk (q : ℚ) (hq) : NNRat.cast ⟨q, hq⟩ = q := rfl

Canonical Embedding of Nonnegative Rational Subtype into Rationals

Informal description

For any rational number $q$ with a proof $hq$ that $q \geq 0$, the canonical embedding of the nonnegative rational number $\langle q, hq \rangle$ into $\mathbb{Q}$ equals $q$.

NNRat.forall theorem

{p : ℚ≥0 → Prop} : (∀ q, p q) ↔ ∀ q hq, p ⟨q, hq⟩

Full source

lemma «forall» {p : ℚ≥0 → Prop} : (∀ q, p q) ↔ ∀ q hq, p ⟨q, hq⟩ := Subtype.forall

Universal Quantification over Nonnegative Rationals via Subtype

Informal description

For any predicate $p$ on nonnegative rational numbers $\mathbb{Q}_{\geq 0}$, the universal quantification $(\forall q \in \mathbb{Q}_{\geq 0}, p(q))$ holds if and only if for every rational number $q \geq 0$ and proof $hq$ that $q \geq 0$, the predicate $p(\langle q, hq \rangle)$ holds.

NNRat.exists theorem

{p : ℚ≥0 → Prop} : (∃ q, p q) ↔ ∃ q hq, p ⟨q, hq⟩

Full source

lemma «exists» {p : ℚ≥0 → Prop} : (∃ q, p q) ↔ ∃ q hq, p ⟨q, hq⟩ := Subtype.exists

Existence in Nonnegative Rationals via Underlying Rationals

Informal description

For any predicate $p$ on nonnegative rational numbers, there exists a nonnegative rational number $q$ satisfying $p(q)$ if and only if there exists a rational number $q$ with $0 \leq q$ such that $p$ holds for the subtype element $\langle q, hq \rangle$ where $hq$ is a proof that $0 \leq q$.

Rat.toNNRat definition

(q : ℚ) : ℚ≥0

Full source

/-- Reinterpret a rational number `q` as a non-negative rational number. Returns `0` if `q ≤ 0`. -/
def _root_.Rat.toNNRat (q : ℚ) : ℚ≥0 :=
  ⟨max q 0, le_max_right _ _⟩

Conversion from rational to nonnegative rational numbers

Informal description

The function takes a rational number $q$ and returns the nonnegative rational number obtained by taking the maximum of $q$ and $0$. If $q \leq 0$, the result is $0$.

Rat.coe_toNNRat theorem

(q : ℚ) (hq : 0 ≤ q) : (q.toNNRat : ℚ) = q

Full source

theorem _root_.Rat.coe_toNNRat (q : ℚ) (hq : 0 ≤ q) : (q.toNNRat : ℚ) = q :=
  max_eq_left hq

Embedding of Nonnegative Rationals Preserves Nonnegative Rationals

Informal description

For any rational number $q$ with $0 \leq q$, the canonical embedding of the nonnegative rational number obtained from $q$ (via `toNNRat`) back into $\mathbb{Q}$ equals $q$ itself. That is, $\text{toNNRat}(q) = q$ when $q \geq 0$.

Rat.le_coe_toNNRat theorem

(q : ℚ) : q ≤ q.toNNRat

Full source

theorem _root_.Rat.le_coe_toNNRat (q : ℚ) : q ≤ q.toNNRat :=
  le_max_left _ _

Rational Number is Less Than or Equal to its Nonnegative Counterpart

Informal description

For any rational number $q$, it holds that $q$ is less than or equal to its nonnegative counterpart obtained by applying the `toNNRat` function, i.e., $q \leq \text{toNNRat}(q)$.

NNRat.coe_nonneg theorem

(q : ℚ≥0) : (0 : ℚ) ≤ q

Full source

@[simp]
theorem coe_nonneg (q : ℚ≥0) : (0 : ℚ) ≤ q :=
  q.2

Nonnegativity of Canonical Embedding of Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the canonical embedding into $\mathbb{Q}$ satisfies $0 \leq q$.

NNRat.coe_zero theorem

: ((0 : ℚ≥0) : ℚ) = 0

Full source

@[simp, norm_cast] lemma coe_zero : ((0 : ℚ≥0) : ℚ) = 0 := rfl

Embedding of Zero in Nonnegative Rationals

Informal description

The canonical embedding of the zero element of the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ into the rational numbers $\mathbb{Q}$ is equal to zero, i.e., $(0 : \mathbb{Q}_{\geq 0}) = 0$.

NNRat.num_zero theorem

: num 0 = 0

Full source

@[simp] lemma num_zero : num 0 = 0 := rfl

Numerator of Zero in Nonnegative Rationals is Zero

Informal description

The numerator of the nonnegative rational number $0$ is $0$.

NNRat.den_zero theorem

: den 0 = 1

Full source

@[simp] lemma den_zero : den 0 = 1 := rfl

Denominator of Zero in Nonnegative Rationals is One

Informal description

The denominator of the nonnegative rational number $0$ is equal to $1$.

NNRat.coe_one theorem

: ((1 : ℚ≥0) : ℚ) = 1

Full source

@[simp, norm_cast] lemma coe_one : ((1 : ℚ≥0) : ℚ) = 1 := rfl

Embedding of One in Nonnegative Rationals to Rationals is One

Informal description

The canonical embedding of the nonnegative rational number $1$ into the rational numbers $\mathbb{Q}$ is equal to $1$, i.e., $(1 : \mathbb{Q}_{\geq 0}) = 1$.

NNRat.num_one theorem

: num 1 = 1

Full source

@[simp] lemma num_one : num 1 = 1 := rfl

Numerator of One in Nonnegative Rationals

Informal description

For the nonnegative rational number $1$, its numerator is equal to $1$.

NNRat.den_one theorem

: den 1 = 1

Full source

@[simp] lemma den_one : den 1 = 1 := rfl

Denominator of One in Nonnegative Rationals is One

Informal description

The denominator of the nonnegative rational number $1$ is equal to $1$.

NNRat.coe_add theorem

(p q : ℚ≥0) : ((p + q : ℚ≥0) : ℚ) = p + q

Full source

@[simp, norm_cast]
theorem coe_add (p q : ℚ≥0) : ((p + q : ℚ≥0) : ℚ) = p + q :=
  rfl

Canonical Embedding Preserves Addition in Nonnegative Rationals

Informal description

For any two nonnegative rational numbers $p$ and $q$, the canonical embedding of their sum in $\mathbb{Q}_{\geq 0}$ into $\mathbb{Q}$ is equal to the sum of their embeddings, i.e., $(p + q : \mathbb{Q}) = p + q$.

NNRat.coe_mul theorem

(p q : ℚ≥0) : ((p * q : ℚ≥0) : ℚ) = p * q

Full source

@[simp, norm_cast]
theorem coe_mul (p q : ℚ≥0) : ((p * q : ℚ≥0) : ℚ) = p * q :=
  rfl

Multiplication Compatibility of Nonnegative Rationals Embedding

Informal description

For any two nonnegative rational numbers $p$ and $q$, the canonical embedding of their product in $\mathbb{Q}_{\geq 0}$ into $\mathbb{Q}$ equals the product of their embeddings, i.e., $(p \cdot q)_{\mathbb{Q}} = p_{\mathbb{Q}} \cdot q_{\mathbb{Q}}$.

NNRat.coe_pow theorem

(q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = (q : ℚ) ^ n

Full source

@[simp, norm_cast] lemma coe_pow (q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = (q : ℚ) ^ n :=
  rfl

Power of Nonnegative Rationals Commutes with Canonical Embedding

Informal description

For any nonnegative rational number $q$ and natural number $n$, the canonical embedding of $q^n$ into $\mathbb{Q}$ equals the $n$-th power of the canonical embedding of $q$ in $\mathbb{Q}$, i.e., $\uparrow(q^n) = (\uparrow q)^n$.

NNRat.num_pow theorem

(q : ℚ≥0) (n : ℕ) : (q ^ n).num = q.num ^ n

Full source

@[simp] lemma num_pow (q : ℚ≥0) (n : ℕ) : (q ^ n).num = q.num ^ n := by simp [num, Int.natAbs_pow]

Power of Numerator in Nonnegative Rationals: $\text{num}(q^n) = (\text{num}(q))^n$

Informal description

For any nonnegative rational number $q$ and natural number $n$, the numerator of $q^n$ is equal to the $n$-th power of the numerator of $q$, i.e., $\text{num}(q^n) = (\text{num}(q))^n$.

NNRat.den_pow theorem

(q : ℚ≥0) (n : ℕ) : (q ^ n).den = q.den ^ n

Full source

@[simp] lemma den_pow (q : ℚ≥0) (n : ℕ) : (q ^ n).den = q.den ^ n := rfl

Denominator of Power of Nonnegative Rational Number Equals Power of Denominator

Informal description

For any nonnegative rational number $q$ and natural number $n$, the denominator of $q^n$ is equal to the $n$-th power of the denominator of $q$, i.e., $\text{den}(q^n) = (\text{den}(q))^n$.

NNRat.coe_sub theorem

(h : q ≤ p) : ((p - q : ℚ≥0) : ℚ) = p - q

Full source

@[simp, norm_cast]
theorem coe_sub (h : q ≤ p) : ((p - q : ℚ≥0) : ℚ) = p - q :=
  max_eq_left <| le_sub_comm.2 <| by rwa [sub_zero]

Embedding of Nonnegative Rational Difference Equals Rational Difference

Informal description

For any nonnegative rational numbers $q$ and $p$ such that $q \leq p$, the canonical embedding of their difference in $\mathbb{Q}_{\geq 0}$ into $\mathbb{Q}$ equals their difference in $\mathbb{Q}$, i.e., $\uparrow(p - q) = p - q$.

NNRat.coe_eq_zero theorem

: (q : ℚ) = 0 ↔ q = 0

Full source

@[simp high]
theorem coe_eq_zero : (q : ℚ) = 0 ↔ q = 0 := by norm_cast

Embedding of Nonnegative Rationals is Zero if and only if Zero

Informal description

For any nonnegative rational number $q$, the canonical embedding of $q$ into $\mathbb{Q}$ equals zero if and only if $q$ itself is zero, i.e., $\uparrow q = 0 \leftrightarrow q = 0$.

NNRat.coe_ne_zero theorem

: (q : ℚ) ≠ 0 ↔ q ≠ 0

Full source

theorem coe_ne_zero : (q : ℚ) ≠ 0(q : ℚ) ≠ 0 ↔ q ≠ 0 :=
  coe_eq_zero.not

Nonzero Embedding of Nonnegative Rationals if and only if Nonzero

Informal description

For any nonnegative rational number $q$, the canonical embedding of $q$ into $\mathbb{Q}$ is nonzero if and only if $q$ itself is nonzero, i.e., $\uparrow q \neq 0 \leftrightarrow q \neq 0$.

NNRat.coe_le_coe theorem

: (p : ℚ) ≤ q ↔ p ≤ q

Full source

@[norm_cast]
theorem coe_le_coe : (p : ℚ) ≤ q ↔ p ≤ q :=
  Iff.rfl

Embedding Preserves Order for Nonnegative Rationals

Informal description

For any nonnegative rational numbers $p$ and $q$, the canonical embedding of $p$ into $\mathbb{Q}$ is less than or equal to that of $q$ if and only if $p \leq q$ in $\mathbb{Q}_{\geq 0}$.

NNRat.coe_lt_coe theorem

: (p : ℚ) < q ↔ p < q

Full source

@[norm_cast]
theorem coe_lt_coe : (p : ℚ) < q ↔ p < q :=
  Iff.rfl

Preservation of strict inequality under canonical embedding of nonnegative rationals

Informal description

For any two nonnegative rational numbers $p$ and $q$, the canonical embedding of $p$ into $\mathbb{Q}$ is less than the canonical embedding of $q$ into $\mathbb{Q}$ if and only if $p < q$ holds in $\mathbb{Q}_{\geq 0}$.

NNRat.coe_pos theorem

: (0 : ℚ) < q ↔ 0 < q

Full source

@[norm_cast]
theorem coe_pos : (0 : ℚ) < q ↔ 0 < q :=
  Iff.rfl

Positivity of Nonnegative Rationals via Canonical Embedding

Informal description

For any nonnegative rational number $q$, the canonical embedding of $0$ into $\mathbb{Q}$ is less than the canonical embedding of $q$ into $\mathbb{Q}$ if and only if $0 < q$ in $\mathbb{Q}_{\geq 0}$.

NNRat.coe_mono theorem

: Monotone ((↑) : ℚ≥0 → ℚ)

Full source

theorem coe_mono : Monotone ((↑) : ℚ≥0 → ℚ) :=
  fun _ _ ↦ coe_le_coe.2

Monotonicity of the Canonical Embedding from Nonnegative Rationals to Rationals

Informal description

The canonical embedding from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to the rational numbers $\mathbb{Q}$ is monotone. That is, for any $p, q \in \mathbb{Q}_{\geq 0}$, if $p \leq q$ in $\mathbb{Q}_{\geq 0}$, then $p \leq q$ in $\mathbb{Q}$.

NNRat.toNNRat_mono theorem

: Monotone toNNRat

Full source

theorem toNNRat_mono : Monotone toNNRat :=
  fun _ _ h ↦ max_le_max h le_rfl

Monotonicity of the Nonnegative Rational Conversion Function

Informal description

The function `toNNRat` from rational numbers to nonnegative rational numbers is monotone, meaning that for any rational numbers $q_1$ and $q_2$ with $q_1 \leq q_2$, we have $\text{toNNRat}(q_1) \leq \text{toNNRat}(q_2)$.

NNRat.toNNRat_coe theorem

(q : ℚ≥0) : toNNRat q = q

Full source

@[simp]
theorem toNNRat_coe (q : ℚ≥0) : toNNRat q = q :=
  ext <| max_eq_left q.2

Identity of Nonnegative Rational Conversion: $\text{toNNRat}(q) = q$ for $q \in \mathbb{Q}_{\geq 0}$

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the conversion of $q$ to a nonnegative rational number via `toNNRat` is equal to $q$ itself, i.e., $\text{toNNRat}(q) = q$.

NNRat.toNNRat_coe_nat theorem

(n : ℕ) : toNNRat n = n

Full source

@[simp]
theorem toNNRat_coe_nat (n : ℕ) : toNNRat n = n :=
  ext <| by simp only [Nat.cast_nonneg', Rat.coe_toNNRat]; rfl

Identity of Natural Number Conversion to Nonnegative Rationals: $\text{toNNRat}(n) = n$

Informal description

For any natural number $n$, the conversion of $n$ to a nonnegative rational number via the function `toNNRat` equals $n$ itself, i.e., $\text{toNNRat}(n) = n$.

NNRat.gi definition

: GaloisInsertion toNNRat (↑)

Full source

/-- `toNNRat` and `(↑) : ℚ≥0 → ℚ` form a Galois insertion. -/
protected def gi : GaloisInsertion toNNRat (↑) :=
  GaloisInsertion.monotoneIntro coe_mono toNNRat_mono Rat.le_coe_toNNRat toNNRat_coe

Galois insertion between rationals and nonnegative rationals

Informal description

The functions `toNNRat` (conversion from rationals to nonnegative rationals) and the canonical embedding `(↑) : ℚ≥0 → ℚ` form a Galois insertion. This means: 1. The embedding is monotone (order-preserving) 2. The conversion function `toNNRat` is monotone 3. For any rational $q$, we have $q \leq \text{toNNRat}(q)$ (the conversion gives an upper bound) 4. For any nonnegative rational $q$, we have $\text{toNNRat}(q) = q$ (the conversion is the identity on nonnegative rationals)

NNRat.coeHom definition

: ℚ≥0 →+* ℚ

Full source

/-- Coercion `ℚ≥0 → ℚ` as a `RingHom`. -/
def coeHom : ℚ≥0ℚ≥0 →+* ℚ where
  toFun := (↑)
  map_one' := coe_one
  map_mul' := coe_mul
  map_zero' := coe_zero
  map_add' := coe_add

Canonical embedding of nonnegative rationals into rationals as a ring homomorphism

Informal description

The canonical ring homomorphism from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to the rational numbers $\mathbb{Q}$, which maps each element to itself. This homomorphism preserves addition, multiplication, zero, and one.

NNRat.coe_natCast theorem

(n : ℕ) : (↑(↑n : ℚ≥0) : ℚ) = n

Full source

@[simp, norm_cast] lemma coe_natCast (n : ℕ) : (↑(↑n : ℚ≥0) : ℚ) = n := rfl

Embedding of Natural Numbers into Nonnegative Rationals Preserves Value

Informal description

For any natural number $n$, the canonical embedding of $n$ as a nonnegative rational number into the rational numbers $\mathbb{Q}$ is equal to $n$ itself, i.e., $\uparrow(\uparrow n : \mathbb{Q}_{\geq 0}) = n$.

NNRat.mk_natCast theorem

(n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), Nat.cast_nonneg' n⟩ : ℚ≥0) n

Full source

@[simp]
theorem mk_natCast (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), Nat.cast_nonneg' n⟩ : ℚ≥0) n :=
  rfl

Canonical Embedding of Natural Numbers into Nonnegative Rationals is Identity

Informal description

For any natural number $n$, the canonical embedding of $n$ into the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ (constructed as $\langle n, \text{Nat.cast\_nonneg' } n \rangle$) is equal to $n$ itself as an element of $\mathbb{Q}_{\geq 0}$.

NNRat.coe_coeHom theorem

: ⇑coeHom = ((↑) : ℚ≥0 → ℚ)

Full source

@[simp]
theorem coe_coeHom : ⇑coeHom = ((↑) : ℚ≥0 → ℚ) :=
  rfl

Canonical Homomorphism Equals Embedding for Nonnegative Rationals

Informal description

The underlying function of the canonical ring homomorphism from nonnegative rationals to rationals is equal to the canonical embedding function, i.e., $\text{coeHom} = (\uparrow : \mathbb{Q}_{\geq 0} \to \mathbb{Q})$.

NNRat.nsmul_coe theorem

(q : ℚ≥0) (n : ℕ) : ↑(n • q) = n • (q : ℚ)

Full source

@[norm_cast]
theorem nsmul_coe (q : ℚ≥0) (n : ℕ) : ↑(n • q) = n • (q : ℚ) :=
  coeHom.toAddMonoidHom.map_nsmul _ _

Scalar Multiplication Commutes with Canonical Embedding of Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any natural number $n \in \mathbb{N}$, the canonical embedding of the $n$-scalar multiple of $q$ into $\mathbb{Q}$ is equal to the $n$-scalar multiple of the canonical embedding of $q$ into $\mathbb{Q}$. In other words, $\uparrow(n \cdot q) = n \cdot (\uparrow q)$.

NNRat.bddAbove_coe theorem

{s : Set ℚ≥0} : BddAbove ((↑) '' s : Set ℚ) ↔ BddAbove s

Full source

theorem bddAbove_coe {s : Set ℚ≥0} : BddAboveBddAbove ((↑) '' s : Set ℚ) ↔ BddAbove s :=
  ⟨fun ⟨b, hb⟩ ↦
    ⟨toNNRat b, fun ⟨y, _⟩ hys ↦
      show y ≤ max b 0 from (hb <| Set.mem_image_of_mem _ hys).trans <| le_max_left _ _⟩,
    fun ⟨b, hb⟩ ↦ ⟨b, fun _ ⟨_, hx, Eq⟩ ↦ Eq ▸ hb hx⟩⟩

Bounded Above Preservation under Canonical Embedding of Nonnegative Rationals

Informal description

For any set $s$ of nonnegative rational numbers, the image of $s$ under the canonical embedding $\mathbb{Q}_{\geq 0} \to \mathbb{Q}$ is bounded above in $\mathbb{Q}$ if and only if $s$ is bounded above in $\mathbb{Q}_{\geq 0}$.

NNRat.bddBelow_coe theorem

(s : Set ℚ≥0) : BddBelow (((↑) : ℚ≥0 → ℚ) '' s)

Full source

theorem bddBelow_coe (s : Set ℚ≥0) : BddBelow (((↑) : ℚ≥0 → ℚ) '' s) :=
  ⟨0, fun _ ⟨q, _, h⟩ ↦ h ▸ q.2⟩

Image of Nonnegative Rationals under Canonical Embedding is Bounded Below

Informal description

For any set $s$ of nonnegative rational numbers, the image of $s$ under the canonical embedding $\mathbb{Q}_{\geq 0} \to \mathbb{Q}$ is bounded below in $\mathbb{Q}$.

NNRat.coe_max theorem

(x y : ℚ≥0) : ((max x y : ℚ≥0) : ℚ) = max (x : ℚ) (y : ℚ)

Full source

@[norm_cast]
theorem coe_max (x y : ℚ≥0) : ((max x y : ℚ≥0) : ℚ) = max (x : ℚ) (y : ℚ) :=
  coe_mono.map_max

Maximum Operation Commutes with Canonical Embedding of Nonnegative Rationals

Informal description

For any nonnegative rational numbers $x$ and $y$, the canonical embedding of their maximum in $\mathbb{Q}_{\geq 0}$ equals the maximum of their embeddings in $\mathbb{Q}$. That is, $\max(x, y) = \max(x, y)$ where the left-hand side is computed in $\mathbb{Q}_{\geq 0}$ and the right-hand side in $\mathbb{Q}$.

NNRat.coe_min theorem

(x y : ℚ≥0) : ((min x y : ℚ≥0) : ℚ) = min (x : ℚ) (y : ℚ)

Full source

@[norm_cast]
theorem coe_min (x y : ℚ≥0) : ((min x y : ℚ≥0) : ℚ) = min (x : ℚ) (y : ℚ) :=
  coe_mono.map_min

Minimum Operation Commutes with Canonical Embedding of Nonnegative Rationals

Informal description

For any nonnegative rational numbers $x$ and $y$, the canonical embedding of their minimum in $\mathbb{Q}_{\geq 0}$ equals the minimum of their embeddings in $\mathbb{Q}$. That is, $\min(x, y) = \min(x, y)$ where the left-hand side is computed in $\mathbb{Q}_{\geq 0}$ and the right-hand side in $\mathbb{Q}$.

NNRat.sub_def theorem

(p q : ℚ≥0) : p - q = toNNRat (p - q)

Full source

theorem sub_def (p q : ℚ≥0) : p - q = toNNRat (p - q) :=
  rfl

Subtraction in Nonnegative Rationals via `toNNRat`

Informal description

For any nonnegative rational numbers $p$ and $q$, the subtraction $p - q$ in $\mathbb{Q}_{\geq 0}$ is equal to the nonnegative rational number obtained by applying the `toNNRat` function to the rational number $p - q$.

NNRat.abs_coe theorem

(q : ℚ≥0) : |(q : ℚ)| = q

Full source

@[simp]
theorem abs_coe (q : ℚ≥0) : |(q : ℚ)| = q :=
  abs_of_nonneg q.2

Absolute Value of Nonnegative Rationals Equals Itself

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the absolute value of its canonical embedding into $\mathbb{Q}$ is equal to itself, i.e., $|q| = q$.

NNRat.nonpos_iff_eq_zero theorem

(q : ℚ≥0) : q ≤ 0 ↔ q = 0

Full source

@[simp high]
theorem nonpos_iff_eq_zero (q : ℚ≥0) : q ≤ 0 ↔ q = 0 :=
  ⟨fun h => le_antisymm h q.2, fun h => h.symm ▸ q.2⟩

Nonnegative Rationals are Zero When Nonpositive

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, $q \leq 0$ if and only if $q = 0$.

Rat.toNNRat_zero theorem

: toNNRat 0 = 0

Full source

@[simp]
theorem toNNRat_zero : toNNRat 0 = 0 := rfl

Conversion of Zero to Nonnegative Rationals

Informal description

The conversion of the rational number $0$ to a nonnegative rational number yields $0$, i.e., $\text{toNNRat}(0) = 0$.

Rat.toNNRat_one theorem

: toNNRat 1 = 1

Full source

@[simp]
theorem toNNRat_one : toNNRat 1 = 1 := rfl

Conversion of One to Nonnegative Rationals: $\text{toNNRat}(1) = 1$

Informal description

The conversion of the rational number $1$ to a nonnegative rational number yields $1$, i.e., $\text{toNNRat}(1) = 1$.

Rat.toNNRat_pos theorem

: 0 < toNNRat q ↔ 0 < q

Full source

@[simp]
theorem toNNRat_pos : 0 < toNNRat q ↔ 0 < q := by simp [toNNRat, ← coe_lt_coe]

Positivity Preservation in Conversion to Nonnegative Rationals

Informal description

For any rational number $q$, the nonnegative rational number obtained by applying the `toNNRat` function to $q$ is positive if and only if $q$ itself is positive, i.e., $0 < \text{toNNRat}(q) \leftrightarrow 0 < q$.

Rat.toNNRat_eq_zero theorem

: toNNRat q = 0 ↔ q ≤ 0

Full source

@[simp]
theorem toNNRat_eq_zero : toNNRattoNNRat q = 0 ↔ q ≤ 0 := by
  simpa [-toNNRat_pos] using (@toNNRat_pos q).not

Zero Condition for Nonnegative Rational Conversion: $\text{toNNRat}(q) = 0 \leftrightarrow q \leq 0$

Informal description

For any rational number $q$, the nonnegative rational number obtained by applying the `toNNRat` function to $q$ is equal to $0$ if and only if $q \leq 0$.

Rat.toNNRat_le_toNNRat_iff theorem

(hp : 0 ≤ p) : toNNRat q ≤ toNNRat p ↔ q ≤ p

Full source

@[simp]
theorem toNNRat_le_toNNRat_iff (hp : 0 ≤ p) : toNNRattoNNRat q ≤ toNNRat p ↔ q ≤ p := by
  simp [← coe_le_coe, toNNRat, hp]

Inequality Preservation in Conversion to Nonnegative Rationals

Informal description

For any rational numbers $q$ and $p$ with $0 \leq p$, the nonnegative rational number obtained from $q$ is less than or equal to the nonnegative rational number obtained from $p$ if and only if $q \leq p$.

Rat.toNNRat_lt_toNNRat_iff' theorem

: toNNRat q < toNNRat p ↔ q < p ∧ 0 < p

Full source

@[simp]
theorem toNNRat_lt_toNNRat_iff' : toNNRattoNNRat q < toNNRat p ↔ q < p ∧ 0 < p := by
  simp [← coe_lt_coe, toNNRat, lt_irrefl]

Inequality of Nonnegative Rational Conversions: $\text{toNNRat}(q) < \text{toNNRat}(p) \leftrightarrow (q < p \land 0 < p)$

Informal description

For any rational numbers $q$ and $p$, the inequality $\text{toNNRat}(q) < \text{toNNRat}(p)$ holds if and only if both $q < p$ and $0 < p$.

Rat.toNNRat_lt_toNNRat_iff theorem

(h : 0 < p) : toNNRat q < toNNRat p ↔ q < p

Full source

theorem toNNRat_lt_toNNRat_iff (h : 0 < p) : toNNRattoNNRat q < toNNRat p ↔ q < p :=
  toNNRat_lt_toNNRat_iff'.trans (and_iff_left h)

Inequality Preservation in Nonnegative Rational Conversion for Positive $p$

Informal description

For any rational numbers $q$ and $p$ with $0 < p$, the inequality $\text{toNNRat}(q) < \text{toNNRat}(p)$ holds if and only if $q < p$.

Rat.toNNRat_lt_toNNRat_iff_of_nonneg theorem

(hq : 0 ≤ q) : toNNRat q < toNNRat p ↔ q < p

Full source

theorem toNNRat_lt_toNNRat_iff_of_nonneg (hq : 0 ≤ q) : toNNRattoNNRat q < toNNRat p ↔ q < p :=
  toNNRat_lt_toNNRat_iff'.trans ⟨And.left, fun h ↦ ⟨h, hq.trans_lt h⟩⟩

Inequality of Nonnegative Rational Conversions for Nonnegative Inputs: $\text{toNNRat}(q) < \text{toNNRat}(p) \leftrightarrow q < p$ when $q \geq 0$

Informal description

For any rational numbers $q$ and $p$ with $0 \leq q$, the inequality $\text{toNNRat}(q) < \text{toNNRat}(p)$ holds if and only if $q < p$.

Rat.toNNRat_add theorem

(hq : 0 ≤ q) (hp : 0 ≤ p) : toNNRat (q + p) = toNNRat q + toNNRat p

Full source

@[simp]
theorem toNNRat_add (hq : 0 ≤ q) (hp : 0 ≤ p) : toNNRat (q + p) = toNNRat q + toNNRat p :=
  NNRat.ext <| by simp [toNNRat, hq, hp, add_nonneg]

Additivity of Nonnegative Rational Conversion for Nonnegative Inputs

Informal description

For any rational numbers $q$ and $p$ such that $0 \leq q$ and $0 \leq p$, the conversion to nonnegative rationals preserves addition, i.e., $\text{toNNRat}(q + p) = \text{toNNRat}(q) + \text{toNNRat}(p)$.

Rat.toNNRat_add_le theorem

: toNNRat (q + p) ≤ toNNRat q + toNNRat p

Full source

theorem toNNRat_add_le : toNNRat (q + p) ≤ toNNRat q + toNNRat p :=
  coe_le_coe.1 <| max_le (add_le_add (le_max_left _ _) (le_max_left _ _)) <| coe_nonneg _

Subadditivity of Nonnegative Rational Conversion: $\text{toNNRat}(q + p) \leq \text{toNNRat}(q) + \text{toNNRat}(p)$

Informal description

For any rational numbers $q$ and $p$, the nonnegative rational conversion of their sum satisfies $\text{toNNRat}(q + p) \leq \text{toNNRat}(q) + \text{toNNRat}(p)$.

Rat.toNNRat_le_iff_le_coe theorem

{p : ℚ≥0} : toNNRat q ≤ p ↔ q ≤ ↑p

Full source

theorem toNNRat_le_iff_le_coe {p : ℚ≥0} : toNNRattoNNRat q ≤ p ↔ q ≤ ↑p :=
  NNRat.gi.gc q p

Characterization of Nonnegative Rational Order: $\text{toNNRat}(q) \leq p \leftrightarrow q \leq p$

Informal description

For any rational number $q$ and any nonnegative rational number $p$, the inequality $\text{toNNRat}(q) \leq p$ holds if and only if $q \leq p$ (where $p$ is viewed as a rational number via the canonical embedding).

Rat.le_toNNRat_iff_coe_le theorem

{q : ℚ≥0} (hp : 0 ≤ p) : q ≤ toNNRat p ↔ ↑q ≤ p

Full source

theorem le_toNNRat_iff_coe_le {q : ℚ≥0} (hp : 0 ≤ p) : q ≤ toNNRat p ↔ ↑q ≤ p := by
  rw [← coe_le_coe, Rat.coe_toNNRat p hp]

Inequality Characterization for Nonnegative Rationals: $q \leq \text{toNNRat}(p) \leftrightarrow \uparrow q \leq p$

Informal description

For any nonnegative rational number $q$ and any rational number $p$ with $0 \leq p$, the inequality $q \leq \text{toNNRat}(p)$ holds if and only if the canonical embedding of $q$ into $\mathbb{Q}$ satisfies $\uparrow q \leq p$.

Rat.le_toNNRat_iff_coe_le' theorem

{q : ℚ≥0} (hq : 0 < q) : q ≤ toNNRat p ↔ ↑q ≤ p

Full source

theorem le_toNNRat_iff_coe_le' {q : ℚ≥0} (hq : 0 < q) : q ≤ toNNRat p ↔ ↑q ≤ p :=
  (le_or_lt 0 p).elim le_toNNRat_iff_coe_le fun hp ↦ by
    simp only [(hp.trans_le q.coe_nonneg).not_le, toNNRat_eq_zero.2 hp.le, hq.not_le]

Positive Nonnegative Rational Order Characterization: $q \leq \text{toNNRat}(p) \leftrightarrow q \leq p$

Informal description

For any positive nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ (i.e., $0 < q$) and any rational number $p \in \mathbb{Q}$, the inequality $q \leq \text{toNNRat}(p)$ holds if and only if $q \leq p$ (where $q$ is viewed as a rational number via the canonical embedding).

Rat.toNNRat_lt_iff_lt_coe theorem

{p : ℚ≥0} (hq : 0 ≤ q) : toNNRat q < p ↔ q < ↑p

Full source

theorem toNNRat_lt_iff_lt_coe {p : ℚ≥0} (hq : 0 ≤ q) : toNNRattoNNRat q < p ↔ q < ↑p := by
  rw [← coe_lt_coe, Rat.coe_toNNRat q hq]

Comparison of Nonnegative Rational Conversion with Original Rational

Informal description

For any nonnegative rational number $p$ and any rational number $q$ with $0 \leq q$, the inequality $\text{toNNRat}(q) < p$ holds if and only if $q < p$ in $\mathbb{Q}$.

Rat.lt_toNNRat_iff_coe_lt theorem

{q : ℚ≥0} : q < toNNRat p ↔ ↑q < p

Full source

theorem lt_toNNRat_iff_coe_lt {q : ℚ≥0} : q < toNNRat p ↔ ↑q < p :=
  NNRat.gi.gc.lt_iff_lt

Comparison of Nonnegative Rational Conversion with Original Rational via Strict Inequality

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$ and any rational number $p \in \mathbb{Q}$, the inequality $q < \text{toNNRat}(p)$ holds if and only if $q < p$ in $\mathbb{Q}$.

Rat.toNNRat_mul theorem

(hp : 0 ≤ p) : toNNRat (p * q) = toNNRat p * toNNRat q

Full source

theorem toNNRat_mul (hp : 0 ≤ p) : toNNRat (p * q) = toNNRat p * toNNRat q := by
  rcases le_total 0 q with hq | hq
  · ext; simp [toNNRat, hp, hq, max_eq_left, mul_nonneg]
  · have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
    rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]

Multiplicativity of Nonnegative Rational Conversion for Nonnegative Inputs

Informal description

For any rational numbers $p$ and $q$ with $0 \leq p$, the conversion to nonnegative rationals satisfies $\text{toNNRat}(p \cdot q) = \text{toNNRat}(p) \cdot \text{toNNRat}(q)$.

Rat.nnabs definition

(x : ℚ) : ℚ≥0

Full source

/-- The absolute value on `ℚ` as a map to `ℚ≥0`. -/
@[pp_nodot]
def Rat.nnabs (x : ℚ) : ℚ≥0 :=
  ⟨abs x, abs_nonneg x⟩

Absolute value of a rational number as a nonnegative rational

Informal description

The function maps a rational number $x$ to its absolute value $\lvert x \rvert$ as a nonnegative rational number.

Rat.coe_nnabs theorem

(x : ℚ) : (Rat.nnabs x : ℚ) = abs x

Full source

@[norm_cast, simp]
theorem Rat.coe_nnabs (x : ℚ) : (Rat.nnabs x : ℚ) = abs x := rfl

Embedding of Nonnegative Absolute Value Equals Absolute Value in Rationals

Informal description

For any rational number $x$, the canonical embedding of its nonnegative absolute value $\text{nnabs}(x)$ into $\mathbb{Q}$ equals the absolute value of $x$, i.e., $\text{nnabs}(x) = |x|$.

NNRat.num_coe theorem

(q : ℚ≥0) : (q : ℚ).num = q.num

Full source

@[norm_cast] lemma num_coe (q : ℚ≥0) : (q : ℚ).num = q.num := by
  simp only [num, Int.natCast_natAbs, Rat.num_nonneg, coe_nonneg, abs_of_nonneg]

Numerator Preservation in Nonnegative Rationals

Informal description

For any nonnegative rational number $q$, the numerator of $q$ when viewed as a rational number is equal to the numerator of $q$ as a natural number, i.e., $\text{num}(q) = \text{num}(q)$.

NNRat.natAbs_num_coe theorem

: (q : ℚ).num.natAbs = q.num

Full source

theorem natAbs_num_coe : (q : ℚ).num.natAbs = q.num := rfl

Absolute Value of Numerator Equals Numerator for Nonnegative Rationals

Informal description

For any nonnegative rational number $q$, the absolute value of the numerator of $q$ (when viewed as a rational number) is equal to the numerator of $q$ (as a natural number). That is, $\text{natAbs}(\text{num}(q)) = \text{num}(q)$.

NNRat.den_coe theorem

: (q : ℚ).den = q.den

Full source

@[norm_cast] lemma den_coe : (q : ℚ).den = q.den := rfl

Denominator Preservation in Nonnegative Rationals

Informal description

For any nonnegative rational number $q$, the denominator of $q$ when viewed as a rational number is equal to the denominator of $q$ as a natural number, i.e., $\text{den}(q) = \text{den}(q)$.

NNRat.num_ne_zero theorem

: q.num ≠ 0 ↔ q ≠ 0

Full source

@[simp] lemma num_ne_zero : q.num ≠ 0q.num ≠ 0 ↔ q ≠ 0 := by simp [num]

Nonzero Numerator Condition for Nonnegative Rationals

Informal description

For any nonnegative rational number $q$, the numerator of $q$ is nonzero if and only if $q$ itself is nonzero.

NNRat.num_pos theorem

: 0 < q.num ↔ 0 < q

Full source

@[simp] lemma num_pos : 0 < q.num ↔ 0 < q := by
  simpa [num, -nonpos_iff_eq_zero] using nonpos_iff_eq_zero _ |>.not.symm

Positivity of Numerator in Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the numerator of $q$ is strictly positive if and only if $q$ itself is strictly positive, i.e., $0 < \text{num}(q) \leftrightarrow 0 < q$.

NNRat.den_pos theorem

(q : ℚ≥0) : 0 < q.den

Full source

@[simp] lemma den_pos (q : ℚ≥0) : 0 < q.den := Rat.den_pos _

Positivity of Denominator for Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the denominator $\text{den}(q)$ is strictly positive, i.e., $0 < \text{den}(q)$.

NNRat.den_ne_zero theorem

(q : ℚ≥0) : q.den ≠ 0

Full source

@[simp] lemma den_ne_zero (q : ℚ≥0) : q.den ≠ 0 := Rat.den_ne_zero _

Nonzero Denominator Property for Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the denominator $\text{den}(q)$ is nonzero.

NNRat.coprime_num_den theorem

(q : ℚ≥0) : q.num.Coprime q.den

Full source

lemma coprime_num_den (q : ℚ≥0) : q.num.Coprime q.den := by simpa [num, den] using Rat.reduced _

Coprimality of Numerator and Denominator in Nonnegative Rationals

Informal description

For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the numerator $\text{num}(q)$ and denominator $\text{den}(q)$ are coprime natural numbers.

NNRat.num_natCast theorem

(n : ℕ) : num n = n

Full source

@[simp, norm_cast] lemma num_natCast (n : ℕ) : num n = n := rfl

Numerator of Natural Number as Nonnegative Rational

Informal description

For any natural number $n$, the numerator of the nonnegative rational number corresponding to $n$ is equal to $n$ itself.

NNRat.den_natCast theorem

(n : ℕ) : den n = 1

Full source

@[simp, norm_cast] lemma den_natCast (n : ℕ) : den n = 1 := rfl

Denominator of Natural Number as Nonnegative Rational is One

Informal description

For any natural number $n$, the denominator of the nonnegative rational number corresponding to $n$ is equal to $1$.

NNRat.num_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : num ofNat(n) = OfNat.ofNat n

Full source

@[simp] lemma num_ofNat (n : ℕ) [n.AtLeastTwo] : num ofNat(n) = OfNat.ofNat n :=
  rfl

Numerator of Nonnegative Rational Number from Natural Number ≥ 2

Informal description

For any natural number $n \geq 2$, the numerator of the nonnegative rational number corresponding to $n$ (via the `OfNat` instance) is equal to $n$ itself.

NNRat.den_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : den ofNat(n) = 1

Full source

@[simp] lemma den_ofNat (n : ℕ) [n.AtLeastTwo] : den ofNat(n) = 1 := rfl

Denominator of Canonical Nonnegative Rational Embedding for $n \geq 2$ is 1

Informal description

For any natural number $n \geq 2$, the denominator of the nonnegative rational number corresponding to $n$ (via the canonical embedding) is equal to 1.

NNRat.ext_num_den theorem

(hn : p.num = q.num) (hd : p.den = q.den) : p = q

Full source

theorem ext_num_den (hn : p.num = q.num) (hd : p.den = q.den) : p = q := by
  refine ext <| Rat.ext ?_ hd
  simpa [num_coe]

Equality of Nonnegative Rationals via Numerator and Denominator

Informal description

For any two nonnegative rational numbers $p$ and $q$, if their numerators are equal ($p.\text{num} = q.\text{num}$) and their denominators are equal ($p.\text{den} = q.\text{den}$), then $p = q$.

NNRat.ext_num_den_iff theorem

: p = q ↔ p.num = q.num ∧ p.den = q.den

Full source

theorem ext_num_den_iff : p = q ↔ p.num = q.num ∧ p.den = q.den :=
  ⟨by rintro rfl; exact ⟨rfl, rfl⟩, fun h ↦ ext_num_den h.1 h.2⟩

Equivalence of Equality and Numerator-Denominator Equality for Nonnegative Rationals

Informal description

Two nonnegative rational numbers $p$ and $q$ are equal if and only if their numerators are equal ($p.\text{num} = q.\text{num}$) and their denominators are equal ($p.\text{den} = q.\text{den}$).

NNRat.divNat definition

(n d : ℕ) : ℚ≥0

Full source

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

See also `Rat.divInt` and `mkRat`. -/
def divNat (n d : ℕ) : ℚ≥0 :=
  ⟨.divInt n d, Rat.divInt_nonneg (Int.ofNat_zero_le n) (Int.ofNat_zero_le d)⟩

Quotient of natural numbers as a nonnegative rational

Informal description

The function constructs a nonnegative rational number as the quotient of two natural numbers $n$ and $d$, represented as $\frac{n}{d}$.

NNRat.coe_divNat theorem

(n d : ℕ) : (divNat n d : ℚ) = .divInt n d

Full source

@[simp, norm_cast] lemma coe_divNat (n d : ℕ) : (divNat n d : ℚ) = .divInt n d := rfl

Embedding of Nonnegative Rational Division into Rationals: $\left(\frac{n}{d} : \mathbb{Q}_{\geq 0}\right) = \frac{n}{d} : \mathbb{Q}$

Informal description

For any natural numbers $n$ and $d$, the canonical embedding of the nonnegative rational number $\frac{n}{d}$ into the rational numbers $\mathbb{Q}$ is equal to the rational number constructed as $\frac{n}{d}$ via the `Rat.divInt` function. That is, $\left(\frac{n}{d} : \mathbb{Q}_{\geq 0}\right) = \frac{n}{d} : \mathbb{Q}$.

NNRat.mk_divInt theorem

(n d : ℕ) : ⟨.divInt n d, Rat.divInt_nonneg (Int.ofNat_zero_le n) (Int.ofNat_zero_le d)⟩ = divNat n d

Full source

lemma mk_divInt (n d : ℕ) :
    ⟨.divInt n d, Rat.divInt_nonneg (Int.ofNat_zero_le n) (Int.ofNat_zero_le d)⟩ = divNat n d := rfl

Construction of Nonnegative Rational via Integer Division Equals Natural Division

Informal description

For any natural numbers $n$ and $d$, the nonnegative rational number constructed as $\langle n/d, h\rangle$ (where $h$ is the proof that $n/d \geq 0$) is equal to the nonnegative rational number obtained via `divNat n d$.

NNRat.divNat_inj theorem

(h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Full source

lemma divNat_inj (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : divNatdivNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁ := by
  rw [← coe_inj]; simp [Rat.mkRat_eq_iff, h₁, h₂]; norm_cast

Equality of Nonnegative Rational Fractions via Cross-Multiplication

Informal description

For any natural numbers $n_1, n_2, d_1, d_2$ with $d_1 \neq 0$ and $d_2 \neq 0$, the equality $\frac{n_1}{d_1} = \frac{n_2}{d_2}$ holds in the nonnegative rational numbers if and only if $n_1 \cdot d_2 = n_2 \cdot d_1$.

NNRat.divNat_zero theorem

(n : ℕ) : divNat n 0 = 0

Full source

@[simp] lemma divNat_zero (n : ℕ) : divNat n 0 = 0 := by simp [divNat]; rfl

Division by Zero Yields Zero in Nonnegative Rationals

Informal description

For any natural number $n$, the nonnegative rational number $\mathrm{divNat}(n, 0)$ is equal to $0$.

NNRat.num_divNat_den theorem

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

Full source

@[simp] lemma num_divNat_den (q : ℚ≥0) : divNat q.num q.den = q :=
  ext <| by rw [← (q : ℚ).mkRat_num_den']; simp [num_coe, den_coe]

Nonnegative Rational as Fraction of Numerator and Denominator

Informal description

For any nonnegative rational number $q$, the fraction $\frac{\text{num}(q)}{\text{den}(q)}$ is equal to $q$ itself, where $\text{num}(q)$ is the numerator of $q$ and $\text{den}(q)$ is its denominator.

NNRat.natCast_eq_divNat theorem

(n : ℕ) : (n : ℚ≥0) = divNat n 1

Full source

lemma natCast_eq_divNat (n : ℕ) : (n : ℚ≥0) = divNat n 1 := (num_divNat_den _).symm

Natural Number Embedding as Nonnegative Rational: $n = \frac{n}{1}$

Informal description

For any natural number $n$, the canonical embedding of $n$ into the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ is equal to the quotient $\frac{n}{1}$.

NNRat.divNat_mul_divNat theorem

 (n₁ n₂ : ℕ) {d₁ d₂} (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) : divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Full source

lemma divNat_mul_divNat (n₁ n₂ : ℕ) {d₁ d₂} (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) :
    divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂) := by
  ext; push_cast; exact Rat.divInt_mul_divInt _ _ (mod_cast hd₁) (mod_cast hd₂)

Multiplication of Nonnegative Rationals via Numerators and Denominators: $ \frac{n_1}{d_1} \cdot \frac{n_2}{d_2} = \frac{n_1 n_2}{d_1 d_2} $

Informal description

For any natural numbers $ n_1, n_2 $ and nonzero natural numbers $ d_1, d_2 $, the product of the nonnegative rational numbers $ \frac{n_1}{d_1} $ and $ \frac{n_2}{d_2} $ is equal to the nonnegative rational number $ \frac{n_1 \cdot n_2}{d_1 \cdot d_2} $.

NNRat.divNat_mul_left theorem

{a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (a * n) (a * d) = divNat n d

Full source

lemma divNat_mul_left {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (a * n) (a * d) = divNat n d := by
  ext; push_cast; exact Rat.divInt_mul_left (mod_cast ha)

Cancellation of Common Factor in Nonnegative Rational Construction: $\frac{a \cdot n}{a \cdot d} = \frac{n}{d}$

Informal description

For any nonzero natural number $a$ and any natural numbers $n$ and $d$, the nonnegative rational number $\frac{a \cdot n}{a \cdot d}$ is equal to $\frac{n}{d}$.

NNRat.divNat_mul_right theorem

{a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (n * a) (d * a) = divNat n d

Full source

lemma divNat_mul_right {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (n * a) (d * a) = divNat n d := by
  ext; push_cast; exact Rat.divInt_mul_right (mod_cast ha)

Cancellation of Common Factor in Nonnegative Rationals: $\frac{n \cdot a}{d \cdot a} = \frac{n}{d}$

Informal description

For any natural number $a \neq 0$ and any natural numbers $n$ and $d$, the nonnegative rational number $\frac{n \cdot a}{d \cdot a}$ is equal to $\frac{n}{d}$.

NNRat.mul_den_eq_num theorem

(q : ℚ≥0) : q * q.den = q.num

Full source

@[simp] lemma mul_den_eq_num (q : ℚ≥0) : q * q.den = q.num := by
  ext
  push_cast
  rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe]
  exact Rat.mul_den_eq_num _

Product of Nonnegative Rational with Denominator Equals Numerator: $q \cdot \text{den}(q) = \text{num}(q)$

Informal description

For any nonnegative rational number $q$, the product of $q$ and its denominator equals its numerator, i.e., $q \cdot \text{den}(q) = \text{num}(q)$.

NNRat.den_mul_eq_num theorem

(q : ℚ≥0) : q.den * q = q.num

Full source

@[simp] lemma den_mul_eq_num (q : ℚ≥0) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num]

Denominator-Numerator Product Identity for Nonnegative Rationals: $\mathrm{den}(q) \cdot q = \mathrm{num}(q)$

Informal description

For any nonnegative rational number $q$, the product of its denominator $\mathrm{den}(q)$ and $q$ equals its numerator $\mathrm{num}(q)$, i.e., $\mathrm{den}(q) \cdot q = \mathrm{num}(q)$.

NNRat.numDenCasesOn definition

{C : ℚ≥0 → Sort u} (q) (H : ∀ n d, d ≠ 0 → n.Coprime d → C (divNat n d)) : C q

Full source

/-- 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. -/
@[elab_as_elim]
def numDenCasesOn.{u} {C : ℚ≥0 → Sort u} (q) (H : ∀ n d, d ≠ 0 → n.Coprime d → C (divNat n d)) :
    C q := by rw [← q.num_divNat_den]; exact H _ _ q.den_ne_zero q.coprime_num_den

Case analysis on numerator and denominator of nonnegative rationals

Informal description

The function provides a way to define a dependent function or prove a universally quantified statement about nonnegative rational numbers by considering them in the form $\frac{n}{d}$ where $d \neq 0$ and $n$, $d$ are coprime natural numbers. Specifically, given a dependent type $C : \mathbb{Q}_{\geq 0} \to \text{Sort } u$ and a nonnegative rational number $q$, if for all natural numbers $n$ and $d$ with $d \neq 0$ and $n$ coprime to $d$, we have $C(\frac{n}{d})$, then we can conclude $C(q)$.

NNRat.add_def theorem

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

Full source

lemma add_def (q r : ℚ≥0) : q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den) := by
  ext; simp [Rat.add_def', Rat.mkRat_eq_divInt, num_coe, den_coe]

Addition Formula for Nonnegative Rationals via Cross-Multiplication

Informal description

For any two nonnegative rational numbers $q$ and $r$, their sum $q + r$ is equal to the nonnegative rational number constructed as $\frac{q_{\text{num}} \cdot r_{\text{den}} + r_{\text{num}} \cdot q_{\text{den}}}{q_{\text{den}} \cdot r_{\text{den}}}$, where $q_{\text{num}}$ and $r_{\text{num}}$ are the numerators, and $q_{\text{den}}$ and $r_{\text{den}}$ are the denominators of $q$ and $r$ respectively.

NNRat.mul_def theorem

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

Full source

lemma mul_def (q r : ℚ≥0) : q * r = divNat (q.num * r.num) (q.den * r.den) := by
  ext; simp [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, num_coe, den_coe]

Product of Nonnegative Rationals via Numerator and Denominator Multiplication

Informal description

For any two nonnegative rational numbers $q$ and $r$, their product $q \cdot r$ is equal to the nonnegative rational number obtained by dividing the product of their numerators $q_\text{num} \cdot r_\text{num}$ by the product of their denominators $q_\text{den} \cdot r_\text{den}$.

NNRat.lt_def theorem

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

Full source

theorem lt_def {p q : ℚ≥0} : p < q ↔ p.num * q.den < q.num * p.den := by
  rw [← NNRat.coe_lt_coe, Rat.lt_def]; norm_cast

Cross-Multiplication Criterion for Strict Order on Nonnegative Rationals

Informal description

For any two nonnegative rational numbers $p$ and $q$, the strict inequality $p < q$ holds if and only if the product of the numerator of $p$ and the denominator of $q$ is strictly less than the product of the numerator of $q$ and the denominator of $p$, i.e., $\text{num}(p) \cdot \text{den}(q) < \text{num}(q) \cdot \text{den}(p)$.

NNRat.le_def theorem

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

Full source

theorem le_def {p q : ℚ≥0} : p ≤ q ↔ p.num * q.den ≤ q.num * p.den := by
  rw [← NNRat.coe_le_coe, Rat.le_def]; norm_cast

Cross-Multiplication Criterion for Nonnegative Rational Order

Informal description

For any two nonnegative rational numbers $p$ and $q$, the inequality $p \leq q$ holds if and only if the product of the numerator of $p$ and the denominator of $q$ is less than or equal to the product of the numerator of $q$ and the denominator of $p$, i.e., $\text{num}(p) \cdot \text{den}(q) \leq \text{num}(q) \cdot \text{den}(p)$.

Mathlib.Tactic.Qify.nnratCast_eq theorem

(a b : ℚ≥0) : a = b ↔ (a : ℚ) = (b : ℚ)

Full source

@[qify_simps] lemma nnratCast_eq (a b : ℚ≥0) : a = b ↔ (a : ℚ) = (b : ℚ) := NNRat.coe_inj.symm

Equality of Nonnegative Rationals via Canonical Embedding

Informal description

For any two nonnegative rational numbers $a$ and $b$, the equality $a = b$ holds if and only if their canonical embeddings into $\mathbb{Q}$ satisfy $(a : \mathbb{Q}) = (b : \mathbb{Q})$.

Mathlib.Tactic.Qify.nnratCast_le theorem

(a b : ℚ≥0) : a ≤ b ↔ (a : ℚ) ≤ (b : ℚ)

Full source

@[qify_simps] lemma nnratCast_le (a b : ℚ≥0) : a ≤ b ↔ (a : ℚ) ≤ (b : ℚ) := NNRat.coe_le_coe.symm

Order Preservation under Canonical Embedding of Nonnegative Rationals

Informal description

For any two nonnegative rational numbers $a$ and $b$, the inequality $a \leq b$ holds if and only if their canonical embeddings into $\mathbb{Q}$ satisfy $(a : \mathbb{Q}) \leq (b : \mathbb{Q})$.

Mathlib.Tactic.Qify.nnratCast_lt theorem

(a b : ℚ≥0) : a < b ↔ (a : ℚ) < (b : ℚ)

Full source

@[qify_simps] lemma nnratCast_lt (a b : ℚ≥0) : a < b ↔ (a : ℚ) < (b : ℚ) := NNRat.coe_lt_coe.symm

Preservation of Strict Inequality under Canonical Embedding of Nonnegative Rationals

Informal description

For any two nonnegative rational numbers $a$ and $b$, the inequality $a < b$ holds if and only if their canonical embeddings into $\mathbb{Q}$ satisfy $(a : \mathbb{Q}) < (b : \mathbb{Q})$.

Mathlib.Tactic.Qify.nnratCast_ne theorem

(a b : ℚ≥0) : a ≠ b ↔ (a : ℚ) ≠ (b : ℚ)

Full source

@[qify_simps] lemma nnratCast_ne (a b : ℚ≥0) : a ≠ ba ≠ b ↔ (a : ℚ) ≠ (b : ℚ) := NNRat.ne_iff.symm

Inequality Preservation under Canonical Embedding of Nonnegative Rationals

Informal description

For any two nonnegative rational numbers $a$ and $b$, we have $a \neq b$ if and only if their canonical embeddings in $\mathbb{Q}$ satisfy $(a : \mathbb{Q}) \neq (b : \mathbb{Q})$.

Mathlib.Data.NNRat.Defs

Notation

Huge warning