Documentation

Mathlib.Data.Rat.Init

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.

source
def termℚ :
Lean.ParserDescr

Rational numbers, implemented as a pair of integers num / den such that the denominator is positive and the numerator and denominator are coprime.

Equations
source
def NNRat :
Type

Nonnegative rational numbers.

Equations
Instances For
source
def «termℚ≥0» :
Lean.ParserDescr

Nonnegative rational numbers.

Equations

Cast from NNRat #

This section sets up the typeclasses necessary to declare the canonical embedding ℚ≥0 to any semifield.

source
class NNRatCast (K : Type u_1) :
Type u_1

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.

  • nnratCast : ℚ≥0 → K

    The canonical homomorphism ℚ≥0 → K.

    Do not use directly. Use the coercion instead.

Instances
source
instance NNRat.instNNRatCast :
NNRatCast ℚ≥0
Equations
source
@[reducible, match_pattern]
def NNRat.cast {K : Type u_1} [NNRatCast K] :
ℚ≥0 → K

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

This is just the bare function in order to aid in creating instances of DivisionSemiring.

Equations
Instances For
source
instance NNRatCast.toCoeTail {K : Type u_1} [NNRatCast K] :
CoeTail ℚ≥0 K
Equations
source
instance NNRatCast.toCoeHTCT {K : Type u_1} [NNRatCast K] :
CoeHTCT ℚ≥0 K
Equations
source
instance Rat.instNNRatCast :
NNRatCast ℚ
Equations

Numerator and denominator of a nonnegative rational #

source
def NNRat.num (q : ℚ≥0) :
ℕ

The numerator of a nonnegative rational.

Equations
source
def NNRat.den (q : ℚ≥0) :
ℕ

The denominator of a nonnegative rational.

Equations
source
@[simp]
theorem NNRat.num_mk (q : ℚ) (hq : 0 ≤ q) :
num ⟨q, hq⟩ = q.num.natAbs
source
@[simp]
theorem NNRat.den_mk (q : ℚ) (hq : 0 ≤ q) :
den ⟨q, hq⟩ = q.den
source
theorem NNRat.cast_id (n : ℚ≥0) :
↑n = n
source
@[simp]
theorem NNRat.cast_eq_id :
NNRat.cast = id
source
theorem Rat.cast_id (n : ℚ) :
↑n = n
source
@[simp]
theorem Rat.cast_eq_id :
Rat.cast = id