mathlib3 documentation


The definition of the Rational Numbers #

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

Summary #

We define a rational number q as a structure { num, denom, pos, cop }, where

Basic constructions and results are set up in data.rat.defs. As we transition to Lean 4, these two files can probably be merged again, as so much of the needed material will be in Std4 anyway.

For now, this split allows us to give the definitions of division rings and fields without significant theory imports.

The definition of the field structure on will be done in data.rat.basic once the field class has been defined.

Main Definitions #

Notations #

Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom

structure rat  :

rat, or , is the type of rational numbers. It is defined as the set of pairs ⟨n, d⟩ of integers such that d is positive and n and d are coprime. This representation is preferred to the quotient because without periodic reduction, the numerator and denominator can grow exponentially (for example, adding 1/2 to itself repeatedly).

Instances for rat

String representation of a rational numbers, used in has_repr, has_to_string, and has_to_format instances.

@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem rat.ext_iff {p q : } :
p = q p.num = q.num p.denom = q.denom
theorem rat.ext {p q : } (hn : p.num = q.num) (hd : p.denom = q.denom) :
p = q