Mathlib.Data.Rat.Init

Module docstring

{"# Basic definitions around the rational numbers

This file declares ℚ notation for the rationals and defines the nonnegative rationals ℚ≥0.

This file is eligible to upstreaming to Batteries. ","### Cast from NNRat

This section sets up the typeclasses necessary to declare the canonical embedding ℚ≥0 to any semifield. ","### Numerator and denominator of a nonnegative rational "}

termℚ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] notation "ℚ" => Rat

Rational numbers notation

Informal description

The notation `ℚ` represents the type of rational numbers, which is defined as `Rat` in Lean.

NNRat definition

Full source

/-- Nonnegative rational numbers. -/
def NNRat := {q : ℚ // 0 ≤ q}

Nonnegative rational numbers

Informal description

The type of nonnegative rational numbers, defined as the subtype of rational numbers $\mathbb{Q}$ consisting of elements $q$ such that $0 \leq q$.

termℚ≥0 definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] notation "ℚ≥0" => NNRat

Notation for nonnegative rational numbers

Informal description

The notation `ℚ≥0` is defined as a shorthand for the type of nonnegative rational numbers, `NNRat`.

NNRatCast structure

(K : Type*)

Full source

/-- Typeclass for the canonical homomorphism `ℚ≥0 → K`.

This should be considered as a notation typeclass. The sole purpose of this typeclass is to be
extended by `DivisionSemiring`. -/
class NNRatCast (K : Type*) where
  /-- The canonical homomorphism `ℚ≥0 → K`.

  Do not use directly. Use the coercion instead. -/
  protected nnratCast : ℚ≥0 → K

Canonical homomorphism from nonnegative rationals

Informal description

The typeclass `NNRatCast` defines the canonical homomorphism from the nonnegative rational numbers `ℚ≥0` to a type `K`. This is primarily a notation typeclass intended to be extended by `DivisionSemiring` to provide the embedding of nonnegative rationals into semifields.

NNRat.instNNRatCast instance

: NNRatCast ℚ≥0

Full source

instance NNRat.instNNRatCast : NNRatCast ℚ≥0 where nnratCast q := q

Identity Homomorphism for Nonnegative Rationals

Informal description

The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ have a canonical homomorphism structure to themselves, given by the identity map.

NNRat.cast definition

: ℚ≥0 → K

Full source

/-- Canonical homomorphism from `ℚ≥0` to a division semiring `K`.

This is just the bare function in order to aid in creating instances of `DivisionSemiring`. -/
@[coe, reducible, match_pattern] protected def NNRat.cast : ℚ≥0 → K := NNRatCast.nnratCast

Canonical homomorphism from nonnegative rationals to a division semiring

Informal description

The canonical homomorphism from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to a division semiring $K$. This function is the underlying map used to define the embedding of nonnegative rationals into $K$ when $K$ is a division semiring.

NNRatCast.toCoeTail instance

[NNRatCast K] : CoeTail ℚ≥0 K

Full source

instance NNRatCast.toCoeTail [NNRatCast K] : CoeTail ℚ≥0 K where coe := NNRat.cast

Tail-Coercion from Nonnegative Rationals to Type with NNRatCast

Informal description

For any type $K$ with a canonical homomorphism from nonnegative rational numbers, there is a tail-coercion from $\mathbb{Q}_{\geq 0}$ to $K$.

NNRatCast.toCoeHTCT instance

[NNRatCast K] : CoeHTCT ℚ≥0 K

Full source

instance NNRatCast.toCoeHTCT [NNRatCast K] : CoeHTCT ℚ≥0 K where coe := NNRat.cast

Head-Coercion from Nonnegative Rationals to Type with NNRatCast

Informal description

For any type $K$ with a canonical homomorphism from nonnegative rational numbers, there is a head-coercion from $\mathbb{Q}_{\geq 0}$ to $K$.

Rat.instNNRatCast instance

: NNRatCast ℚ

Full source

instance Rat.instNNRatCast : NNRatCast ℚ := ⟨Subtype.val⟩

Canonical Homomorphism from Nonnegative Rationals to Rationals

Informal description

The rational numbers $\mathbb{Q}$ are equipped with a canonical homomorphism from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$.

NNRat.num definition

(q : ℚ≥0) : ℕ

Full source

/-- The numerator of a nonnegative rational. -/
def num (q : ℚ≥0) : ℕ := (q : ℚ).num.natAbs

Numerator of a nonnegative rational number

Informal description

For a nonnegative rational number $ q $, the function returns the numerator of $ q $ as a natural number, which is the absolute value of the numerator of $ q $ viewed as a rational number.

NNRat.den definition

(q : ℚ≥0) : ℕ

Full source

/-- The denominator of a nonnegative rational. -/
def den (q : ℚ≥0) : ℕ := (q : ℚ).den

Denominator of a nonnegative rational number

Informal description

The function maps a nonnegative rational number $ q $ to its denominator as a natural number, which is the denominator of $ q $ viewed as a rational number.

NNRat.num_mk theorem

(q : ℚ) (hq : 0 ≤ q) : num ⟨q, hq⟩ = q.num.natAbs

Full source

@[simp] lemma num_mk (q : ℚ) (hq : 0 ≤ q) : num ⟨q, hq⟩ = q.num.natAbs := rfl

Numerator of Nonnegative Rational Construction: $\text{num}(\langle q, hq \rangle) = |\text{num}(q)|_{\mathbb{N}}$

Informal description

For any rational number $q$ with $0 \leq q$, the numerator of the nonnegative rational number $\langle q, hq \rangle$ (constructed from $q$ and its nonnegativity proof $hq$) is equal to the absolute value of the numerator of $q$ as a natural number, i.e., $\text{num}(\langle q, hq \rangle) = |\text{num}(q)|_{\mathbb{N}}$.

NNRat.den_mk theorem

(q : ℚ) (hq : 0 ≤ q) : den ⟨q, hq⟩ = q.den

Full source

@[simp] lemma den_mk (q : ℚ) (hq : 0 ≤ q) : den ⟨q, hq⟩ = q.den := rfl

Denominator of Nonnegative Rational Construction: $\text{den}(\langle q, hq \rangle) = \text{den}(q)$

Informal description

For any rational number $q$ with $0 \leq q$, the denominator of the nonnegative rational number $\langle q, hq \rangle$ (constructed from $q$ and its nonnegativity proof $hq$) is equal to the denominator of $q$.

NNRat.cast_id theorem

(n : ℚ≥0) : NNRat.cast n = n

Full source

@[norm_cast] lemma cast_id (n : ℚ≥0) : NNRat.cast n = n := rfl

Identity of Nonnegative Rational Number Embedding: $\text{cast}(n) = n$

Informal description

For any nonnegative rational number $n \in \mathbb{Q}_{\geq 0}$, the canonical embedding of $n$ into $\mathbb{Q}_{\geq 0}$ (via `NNRat.cast`) is equal to $n$ itself, i.e., $\text{cast}(n) = n$.

NNRat.cast_eq_id theorem

: NNRat.cast = id

Full source

@[simp] lemma cast_eq_id : NNRat.cast = id := rfl

Nonnegative Rational Cast is Identity Function

Informal description

The canonical homomorphism from nonnegative rational numbers to themselves is equal to the identity function, i.e., $\text{NNRat.cast} = \text{id}$.

Rat.cast_id theorem

(n : ℚ) : Rat.cast n = n

Full source

@[norm_cast] lemma cast_id (n : ℚ) : Rat.cast n = n := rfl

Identity of Rational Number Embedding: $\text{cast}(n) = n$

Informal description

For any rational number $n \in \mathbb{Q}$, the canonical embedding of $n$ into $\mathbb{Q}$ (via `Rat.cast`) is equal to $n$ itself, i.e., $\text{cast}(n) = n$.

Rat.cast_eq_id theorem

: Rat.cast = id

Full source

@[simp] lemma cast_eq_id : Rat.cast = id := rfl

Rational Cast is Identity Function

Informal description

The canonical embedding from the rational numbers to themselves is equal to the identity function.