Numbers

InductiveNatural number #

The natural numbers are the numbers $0, 1, 2, 3, \dots$ used to count the elements of finite collections and to number the positions in a sequence. Their collection is written $\mathbb{N}$. They are where arithmetic begins: the integers, the rational numbers and the real numbers are all constructed from them, and proof by induction, one of the basic methods of mathematical argument, is a property of $\mathbb{N}$. Conventions differ on whether $0$ counts as a natural number; this article, like Mathlib, includes it, and calls $1, 2, 3, \dots$ the positive integers.

Definition

The natural numbers are characterized by the Peano axioms. They form a set $\mathbb{N}$ with a distinguished element $0$ and a successor function $S \colon \mathbb{N} \to \mathbb{N}$, thought of as $n \mapsto n + 1$, such that:

$0$ is not the successor of any natural number: $S(n) \neq 0$ for every $n$;
the successor function is injective: $S(m) = S(n)$ implies $m = n$;
induction holds: if a set of natural numbers contains $0$, and contains $S(n)$ whenever it contains $n$, then it contains every natural number.

Any two structures satisfying these axioms are isomorphic by a unique bijection that matches the two zeros and the two successor functions, so the axioms determine $\mathbb{N}$ up to isomorphism. This uniqueness needs induction for every subset of $\mathbb{N}$; with induction only for first-order formulas, nonstandard models exist. In set theory one concrete model takes $0$ to be the empty set and $S(n) = n \cup \{n\}$, so that each natural number is the set of all smaller natural numbers, $n = \{0, 1, \dots, n - 1\}$.

The same principle that justifies induction also justifies definition by recursion: given a value $a$ and a rule $g$, there is exactly one function $f$ on $\mathbb{N}$ with $f(0) = a$ and $f(n + 1) = g(n, f(n))$ for every $n$. Addition and multiplication are defined this way, by recursion on the second argument:

\[m + 0 = m, \qquad m + S(n) = S(m + n), \qquad m \cdot 0 = 0, \qquad m \cdot S(n) = m \cdot n + m.\]

Writing $1 = S(0)$, the first two equations give $S(n) = n + 1$.

Properties

Arithmetic. Under these operations the natural numbers form a commutative semiring: addition and multiplication are associative and commutative, multiplication distributes over addition, and $0$ and $1$ are the identity elements. No natural number other than $0$ has an additive inverse, so the equation $m + x = n$ need not have a solution in $\mathbb{N}$; adjoining the missing solutions produces the integers.

Order. The usual order is determined by addition: $m \le n$ holds exactly when $n = m + k$ for some natural number $k$. Every sum $m + k$ is at least $m$, and whenever $m \le n$ there is such a $k$. This is a total order in which $0$ is the least element and there is no largest element, since $n < n + 1$.

Well-ordering. Every nonempty set $A$ of natural numbers has a least element: the infimum of $A$ belongs to $A$ and lies below every element of $A$. The well-ordering principle can stand in for induction: to prove that a property holds everywhere, one shows that a least counterexample cannot exist.

Division with remainder. For natural numbers $a$ and $b$ with $b > 0$ there are natural numbers $q$ and $r$, the quotient and the remainder, with

\[a = bq + r, \qquad 0 \le r < b.\]

Taking $q = \lfloor a / b \rfloor$ and $r = a \bmod b$, the identity $b \lfloor a/b \rfloor + (a \bmod b) = a$ holds, and the remainder is less than $b$ when $b > 0$. Repeated division with remainder is the Euclidean algorithm, which computes the greatest common divisor.

Primes. A natural number $p \ge 2$ is prime if its only divisors are $1$ and $p$. There are infinitely many primes: for every $n$ there is a prime $p \ge n$. By the fundamental theorem of arithmetic, every positive integer is a product of primes, and any two factorizations of $n$ into primes differ only in the order of the factors.

Size. The set $\mathbb{N}$ is infinite, and its cardinality is $\aleph_0$, the smallest infinite cardinal (see aleph numbers). A set is countable when it can be mapped injectively into $\mathbb{N}$.

Induction and recursion

Several variants of induction follow from the axiom. In strong induction, if a property holds for $n$ whenever it holds for every $m < n$, then it holds for every natural number. Induction can also start at any base value $m$: if a property holds for $m$, and passes from $n$ to $n + 1$ for every $n \ge m$, then it holds for every $n \ge m$.

Recursion defines most of the familiar functions and sequences of elementary mathematics: powers by $a^0 = 1$ and $a^{n+1} = a^n \cdot a$, the factorial by $0! = 1$ and $(n + 1)! = (n + 1) \cdot n!$, and the Fibonacci numbers by $F_0 = 0$, $F_1 = 1$ and $F_{n+2} = F_n + F_{n+1}$. A recurrent sequence of real numbers, given by a first term $x_0$ and a rule $x_{n+1} = h(x_n)$, is a function on $\mathbb{N}$ defined in the same way.

Number systems. The integers adjoin additive inverses, the rational numbers multiplicative inverses of nonzero integers, and the real numbers limits of Cauchy sequences of rationals.
Semirings. For every semiring $R$ there is a ring homomorphism from $\mathbb{N}$ to $R$ sending $n$ to $n \cdot 1$, and any two ring homomorphisms from $\mathbb{N}$ to $R$ are equal. So $\mathbb{N}$ is the initial object among semirings: it maps to every semiring by exactly one homomorphism.
Ordinals and cardinals. In the set-theoretic model above, the natural numbers are exactly the finite ordinals, and they also serve as the finite cardinals.

In Mathlib

The natural numbers are defined in Lean's core library as an inductive type with two constructors, zero and successor. Lean generates the recursion principle together with this definition, so nothing has to be postulated as an axiom; induction is that recursion principle applied to a family of propositions, and the other two Peano axioms are theorems. The kernel computes with natural numbers using arbitrary-precision arithmetic. Zero is a natural number, and the positive natural numbers form a separate type. The operations are total, with conventions for the cases where the textbook operation is undefined: subtraction is truncated, so that $m - n = 0$ exactly when $m \le n$ (for instance $3 - 5 = 0$); division rounds down, and division by zero gives $0$, while the remainder of $a$ on division by zero is $a$. Statements that need genuine subtraction carry a hypothesis such as $n \le m$, or pass to the integers. Mathlib reads a natural number as an element of any semiring through the cast $n \mapsto n \cdot 1$, which the map above bundles as a ring homomorphism; this is how numerals such as $2$ make sense in every ring.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibNat

Uses 1 · Used by 94

Statement usesSet

Used byThe Infinitude of Primes · Königsberg Bridges Problem · The Binomial Theorem · The Number of Subsets of a Set · The Partition Theorem · Ascending or Descending Sequences (Erdős–Szekeres Theorem) · Formula for the Number of Combinations · Sum of an arithmetic series · The Perfect Number Theorem · Bertrand’s Postulate · Divisibility by 3 Rule · The Friendship Theorem · Sigma-algebra · Bornology · Additive energy · Freiman homomorphisms · Sets without arithmetic progressions · Bell numbers · Catalan numbers · Dyck words · Adjacency matrix · Degree-sum formula · Strongly regular graphs · Turán's theorem · Finite · Infinite · Strong pigeonhole principle · Hales-Jewett theorem · Van der Waerden theorem · Four functions theorem · Harris-Kleitman inequality · Kleitman's theorem · Kruskal-Katona theorem · Maximum size of an intersecting family · Sperner's theorem · VC dimension · Hall's marriage theorem · Stream · Finitely supported function · Hash map · Size-balanced binary search tree · Periodic points · Euclidean domain · Euclid's' algorithm · Euler's totient function ($\varphi$) · Least common multiple · Characteristic of a ring · Characteristic p · Characteristic zero · Arithmetic functions · Matiyasevič's theorem · Solutions to Pell's equation (Number theory) · Sum of four squares · Integer · Rational number · Locally ringed space · Prime spectrum · Convex cone · Module · Ackermann function · In terms of general recursive functions · In terms of Turing machines · Primitive recursive function · Turing degrees · Arden's lemma · First-order formula · First-order structure · Aleph numbers · Beth numbers · Cantor normal form · Epsilon numbers · Gamma numbers · Sequential space · Sequential compactness is equivalent to compactness (Bolzano-Weierstrass) · Infinite sum · Jordan–Hölder theorem · Squeeze theorem · Myhill–Nerode theorem · Erdős–Ko–Rado theorem · Multinomial theorem · Tutte theorem · Cantor's isomorphism theorem · Kleene fixed-point theorem · Kleene's recursion theorem · König's theorem (set theory) · Metrization theorems · Glaisher's theorem · Zeckendorf's theorem · Convex subsets · Extreme point · Order of an element · Direct sum · Invertible elements · Prime numbers

InductiveInteger #

The integers are the whole numbers $\dots, -2, -1, 0, 1, 2, \dots$: the natural numbers, their negatives, and zero. Together they form a set written $\mathbb{Z}$. They extend the natural numbers so that subtraction is always possible, and they are the basic example of a commutative ring. Divisibility, primes and congruences are studied in $\mathbb{Z}$, and every ring receives exactly one structure-preserving map from it.

Definition

One standard construction builds $\mathbb{Z}$ from the natural numbers by formal differences. A pair $(a, b)$ of natural numbers stands for $a - b$, and two pairs $(a, b)$ and $(c, d)$ are identified when $a + d = b + c$. Addition and multiplication are given by

\[(a, b) + (c, d) = (a + c,\ b + d), \qquad (a, b)\,(c, d) = (ac + bd,\ ad + bc),\]

and these rules respect the identification. The natural number $n$ is the class of $(n, 0)$, and the negative of the class of $(a, b)$ is the class of $(b, a)$.

Every class contains a pair with a zero entry, so each integer is either a natural number $n$ or a negative number $-(n + 1)$ with $n$ natural, and never both. This description can itself serve as the definition, and it is the one used for the integers in Lean.

Algebraic structure

With the usual operations, $\mathbb{Z}$ is a commutative ring (see ring structure on $\mathbb{Z}$): addition and multiplication are associative and commutative with identities $0$ and $1$, every integer $a$ has an additive inverse $-a$, and multiplication distributes over addition. Under addition alone the integers form an abelian group, and the subgroup generated by $1$ is all of $\mathbb{Z}$, so this group is cyclic.

The integers form an integral domain: $0 \neq 1$, and a product $ab$ is zero only when $a = 0$ or $b = 0$. Multiplicative inverses are rare: an integer is invertible in $\mathbb{Z}$ exactly when it is $1$ or $-1$.

For every ring $R$ there is a ring homomorphism from $\mathbb{Z}$ to $R$, sending a positive integer $n$ to the sum $1 + \dots + 1$ of $n$ copies of the multiplicative identity $1$ of $R$, $0$ to $0$, and $-n$ to the negative of that sum, and every ring homomorphism from $\mathbb{Z}$ to $R$ equals this one. In the language of categories, $\mathbb{Z}$ is the initial ring. Inverting the nonzero integers gives the rational numbers: $\mathbb{Q}$ is the field of fractions of $\mathbb{Z}$ (see field of fractions).

Order

The integers are totally ordered, and the order is compatible with the ring operations: $a \le b$ implies $a + c \le b + c$, and a product of positive integers is positive; together with $0 < 1$, this makes $\mathbb{Z}$ a strictly ordered ring (see ordered ring, of which this is the strict form).

Unlike the natural numbers, $\mathbb{Z}$ has no least element, but every nonempty set of integers that is bounded below has a least element, and likewise every nonempty set bounded above has a greatest element. Induction extends in both directions: a property that holds for $0$, passes from $n$ to $n + 1$ and from $-n$ to $-n - 1$ for every natural number $n$, holds for every integer.

The set $\mathbb{Z}$ is infinite but can be put in one-to-one correspondence with the natural numbers; one such correspondence lists the integers as $0, -1, 1, -2, 2, \dots$.

Divisibility and primes

For integers $a$ and $b$ with $b \neq 0$ there is exactly one pair of integers $q$, $r$ with $a = bq + r$ and $0 \le r < |b|$, namely the quotient and the remainder of $a$ by $b$. This division with remainder makes $\mathbb{Z}$ a Euclidean domain (see Euclidean domain and $\mathbb{Z}$ is a Euclidean ring). Repeated division computes greatest common divisors, and the greatest common divisor of $a$ and $b$ can be written $ax + by$ for some integers $x$ and $y$, which is Bézout's theorem.

Since every ideal of a Euclidean domain is principal, $\mathbb{Z}$ is a principal ideal domain: its ideals are the sets $n\mathbb{Z}$ of multiples of a natural number $n$. An integer $p$ is prime if it is neither zero nor a unit and, whenever $p$ divides a product $ab$, it divides $a$ or $b$. An integer is prime exactly when its absolute value is a prime natural number, so the primes of $\mathbb{Z}$ are $\pm 2, \pm 3, \pm 5, \dots$. Because every principal ideal domain is a unique factorization domain (see unique factorization domain), every nonzero integer is $\pm 1$ times a product of positive primes (the empty product for $\pm 1$), unique up to the order of the factors: the fundamental theorem of arithmetic.

For a fixed nonzero integer $n$, congruence modulo $n$ relates integers with the same remainder by $n$; $a \equiv b \pmod n$ exactly when $n$ divides $b - a$.

The integers are the first step in the chain $\mathbb{N} \subset \mathbb{Z} \subset \mathbb{Q} \subset \mathbb{R} \subset \mathbb{C}$ leading to the real numbers and the complex numbers. Completing $\mathbb{Z}$ with respect to the $p$-adic absolute value for a prime $p$, under which an integer is small when it is divisible by a high power of $p$, gives the $p$-adic integers.

In Mathlib

The type of integers is defined in Lean's core library rather than in Mathlib, as the second description above: an integer is either a natural number or the negative of the successor of one. Every integer therefore has exactly one representation, and no quotient is needed. The compiler stores small integers directly and larger ones in arbitrary precision. Mathlib supplies the ring, order and Euclidean structures as instances on this type. A natural number is not literally an integer; it becomes one through the cast map, and the absolute value used for primes is a natural number. Division on $\mathbb{Z}$ follows the convention of the remainder theorem above, so the remainder is never negative: $-7$ divided by $2$ gives quotient $-4$ and remainder $1$, rather than the truncated quotient $-3$. Division is total, and dividing by zero gives $0$. The greatest common divisor of two integers is likewise a natural number.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibInt

Uses 1 · Used by 52

Statement usesNatural number

Used byFormula for Pythagorean Triples · Dirichlet’s Theorem · Greatest Common Divisor Algorithm · Derangements Formula · Principle of Inclusion/Exclusion · Cauchy-Davenport theorem · Dyson transform · Erdős–Ginzburg–Ziv theorem · Plünnecke-Petridis inequality · Ruzsa triangle inequality · Turán's theorem · Euclid's' algorithm · Least common multiple · Lucas-Lehmer primality test · Characteristic p · Cyclic group · Structure of finitely generated abelian groups · Solutions to Pell's equation (Number theory) · Sum of four squares · Sum of two squares · Continued fraction · $p$-adic integer · Rational number · Affine space · Scheme · Minimal tensor product · Salient cone · Polar form of a quadratic · Quotient space (Fundamentals) · The category of modules over a ring · Determinant · Completion of an abelian topological group · Topological group · Topological ring · Jacobson density theorem · Binomial inverse theorem · Focal subgroup theorem · Cauchy's theorem (group theory) · Jordan–Hölder theorem · Nielsen–Schreier theorem · Schur–Zassenhaus theorem · Erdős–Ko–Rado theorem · Kleene's recursion theorem · Cross product · Generalized eigenspaces · Bézout's identity · Congruence in $\Z$ · $\Z/n\Z$ and its invertible elements · Product of rings · Ring structure $\Z$ · Newton's identities · Additive subgroups of $\R$

StructureRational number #

A rational number is a number that can be written as a quotient $a/b$ of two integers with $b \neq 0$. The rational numbers form the set $\mathbb{Q}$, the smallest number system that contains the integers and in which division by any nonzero number is always possible. They are the most familiar example of a field, they sit between the integers and the real numbers, and both the real and the $p$-adic numbers are built from them by completion.

Definition

A rational number is determined by a numerator $a \in \mathbb{Z}$ and a nonzero denominator $b \in \mathbb{Z}$, but not uniquely: $1/2$ and $2/4$ name the same number. Two quotients are identified by cross-multiplication: for integers $a, b, c, d$ with $b \neq 0$ and $d \neq 0$, $a/b = c/d$ holds exactly when $ad = cb$. One construction of $\mathbb{Q}$ takes this as its starting point: a rational number is an equivalence class of pairs $(a, b)$ with $b \neq 0$ under the relation $(a, b) \sim (c, d)$ if and only if $ad = cb$.

Each class has a preferred representative. Dividing $a$ and $b$ by their greatest common divisor, and changing both signs if $b < 0$, gives the reduced form $p/q$, with $q > 0$ and $p$ and $q$ coprime. Lean's library defines a rational number to be exactly such a pair: an integer numerator and a positive natural-number denominator with no common factor other than $1$. Every rational number $r$ is the quotient of its numerator by its denominator, and the reduced form is unique: if $a/b = c/d$ with $b, d > 0$, $a$ coprime to $b$ and $c$ coprime to $d$, then $a = c$ and $b = d$. A rational number $r$ has denominator $1$ exactly when $r$ equals its numerator, that is, when $r$ is an integer.

The operations are those of school arithmetic:

\[\frac{a}{b} + \frac{c}{d} = \frac{ad + cb}{bd}, \qquad \frac{a}{b} \cdot \frac{c}{d} = \frac{ac}{bd},\]

and, for positive denominators $b$ and $d$, $a/b \le c/d$ exactly when $ad \le cb$.

Examples

$-6/4$ has reduced form $-3/2$; $0$ has reduced form $0/1$.
Every integer $n$ is rational, as $n/1$.
The terminating decimal $0.75$ is $3/4$, and the repeating decimal $0.333\ldots$ is $1/3$. A real number is rational exactly when its decimal expansion is eventually periodic.
The square root of $2$ is not rational: $\sqrt 2$ is irrational (see irrationality of the square root of 2). If $\sqrt 2 = p/q$ in reduced form, then $p^2 = 2q^2$ forces $p$ and then $q$ to be even, contradicting coprimality.

Properties

Field. With these operations $\mathbb{Q}$ is a field (see field of rational numbers): every nonzero $a/b$ has the inverse $b/a$.
Field of fractions of $\mathbb{Z}$. Every rational number is a quotient of integers, the map from $\mathbb{Z}$ to $\mathbb{Q}$ is injective, and every nonzero integer is invertible in $\mathbb{Q}$, so $\mathbb{Q}$ is the field of fractions of $\mathbb{Z}$ (see field of fractions).
Prime field of characteristic zero. $\mathbb{Q}$ has characteristic zero (see characteristic zero). Conversely, in any field $K$ of characteristic zero the integers $n \cdot 1$ with $n \neq 0$ are invertible, and sending $a/b$ to $(a \cdot 1)(b \cdot 1)^{-1}$ defines a ring homomorphism from $\mathbb{Q}$ to $K$, which is injective. Moreover any two ring homomorphisms from $\mathbb{Q}$ to the same ring are equal. So every field of characteristic zero contains exactly one copy of $\mathbb{Q}$, and that copy is its smallest subfield, the prime subfield.
Ordered field. The order is compatible with the operations: $\mathbb{Q}$ is a strictly ordered ring (see ordered ring), so sums and products of positive rationals are positive. It is Archimedean: every rational number is less than some natural number.
Density. Between any two rationals $r < s$ lies a third, for instance $(r + s)/2$. The rationals are also dense in the reals: $\mathbb{Q}$ is dense in $\mathbb{R}$, and more generally in every Archimedean ordered field with its order topology.
Countability. $\mathbb{Q}$ is countably infinite (see denumerability of the rationals): listing the reduced fractions by increasing $|p| + q$ puts them in bijection with $\mathbb{N}$. Its cardinality is $\aleph_0$.
Order type. Any two countable dense linear orders without endpoints that are nonempty are order-isomorphic (Cantor's isomorphism theorem). Since $\mathbb{Q}$ is such an order, it is, up to order isomorphism, the only one.
Incompleteness. The set of positive rationals $x$ with $x^2 < 2$ is bounded above in $\mathbb{Q}$ but has no least upper bound there. Filling these gaps produces the real numbers, which can be built as equivalence classes of Cauchy sequences of rationals.
Continued fractions. A real number has a terminating continued fraction expansion exactly when it is rational (see continued fraction); the statement holds more generally in any linearly ordered field with a floor function.

Absolute values and completions

Besides the usual absolute value $|x|$, the rationals carry the $p$-adic absolute value for each prime $p$, which is small on numbers divisible by a high power of $p$. Ostrowski's theorem says these are all: every nontrivial real-valued absolute value on $\mathbb{Q}$ is equivalent either to the usual one or to the $p$-adic one for a unique prime $p$. Completing $\mathbb{Q}$ with respect to the usual absolute value gives $\mathbb{R}$; completing with respect to the $p$-adic one gives the field of $p$-adic numbers.

In Mathlib

The type of rational numbers is defined in Lean's core library, not in Mathlib itself, as a structure holding the reduced form: an integer numerator, a natural-number denominator, a proof that the denominator is nonzero, and a proof that numerator and denominator are coprime. Arithmetic operations normalize their results, so equal rational numbers have identical representations and equality can be decided by comparing numerators and denominators. Core Lean also defines the arithmetic operations and the order relation; Mathlib adds the field and ordered-field structure, the topology and the cardinality results. As everywhere in Mathlib, division is a total operation, and dividing by zero gives zero, so $1/0 = 0$ in $\mathbb{Q}$. Mathlib maps rational numbers into any division ring by the same formula as above, a map that is injective in characteristic zero, and it defines an irrational number as a real number not in the image of $\mathbb{Q}$.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibRat

Uses 2 · Used by 39

Statement usesInteger · Natural number

Used byThe Denumerability of the Rational Numbers · Sum of the Reciprocals of the Triangular Numbers · The Solution of a Cubic · The Solution of the General Quartic Equation · Wilson’s Lemma · The Factor and Remainder Theorems · The Friendship Theorem · Carathéodory's theorem · Jensen's inequality (finite sum version) · Doubling constant · Ahlswede-Zhang identity · LYM inequality · Bernoulli numbers · Continued fraction · $p$-adic number · Real number · Finite-dimensionality · Chevalley–Warning theorem (1000+ theorems) · Integral root theorem · Mason–Stothers theorem · Rational root theorem · Schwartz–Zippel theorem · Wedderburn's little theorem · Birkhoff–Von Neumann theorem · Wedderburn–Artin theorem · Lie's theorem · Weierstrass preparation theorem · Commandino's theorem · Radon's theorem · Fermat's little theorem · Sylvester's law of inertia (uniqueness) · Complementary subspaces · Existence of bases · Vector subspace · Irreducible representation · Gaussian elimination · Lagrange interpolation · Field $\Q$ of rational numbers · Rational functions

DefinitionContinued fraction #

A continued fraction is an expression of the form

\[a_0 + \cfrac{1}{a_1 + \cfrac{1}{a_2 + \cfrac{1}{a_3 + \cdots}}}\]

which may stop after finitely many steps or go on forever. In the classical case, usually called a regular continued fraction, $a_0$ is an integer and the later terms $a_1, a_2, \dots$ are positive integers. Every real number has such an expansion, obtained by repeatedly splitting off the integer part and inverting the rest. The expansion stops exactly for rational numbers, and its truncations give unusually good rational approximations, which makes continued fractions a basic tool of Diophantine approximation and of the arithmetic of quadratic irrationals.

Definition

A generalized continued fraction consists of a head term $h$ and a finite or infinite sequence of pairs $(c_i, d_i)$ of partial numerators and partial denominators, and stands for

\[h + \cfrac{c_0}{d_0 + \cfrac{c_1}{d_1 + \cfrac{c_2}{d_2 + \cdots}}}\]

It is simple when every partial numerator equals $1$, and a regular continued fraction is a simple one whose partial denominators are all positive. In this general sense a regular continued fraction need not have integer terms; the classical regular continued fraction above is the case where the head term and the partial denominators are integers, with $h = a_0$ and $d_i = a_{i+1}$, and one writes it $[a_0; a_1, a_2, \dots]$.

The $n$-th convergent of $[a_0; a_1, a_2, \dots]$ is the value $p_n/q_n$ of the truncation $[a_0; a_1, \dots, a_n]$. Its numerator and denominator are computed by the recurrence

\[p_n = a_n p_{n-1} + p_{n-2}, \qquad q_n = a_n q_{n-1} + q_{n-2},\]

starting from $p_{-1} = 1$, $q_{-1} = 0$, $p_0 = a_0$, $q_0 = 1$. For a regular continued fraction with terms in a linearly ordered field, the convergents given by the recurrence equal the values of the truncated fractions.

The expansion of a number

To expand a real number $v$, set $a_0 = \lfloor v \rfloor$. If $v$ is an integer, stop; otherwise $v - a_0$ lies strictly between $0$ and $1$, and one expands $1/(v - a_0) > 1$ in the same way to obtain $a_1, a_2, \dots$. This is the Euclidean algorithm in disguise: for $v = 415/93$ the successive divisions give $415 = 4 \cdot 93 + 43$, $93 = 2 \cdot 43 + 7$, $43 = 6 \cdot 7 + 1$, $7 = 7 \cdot 1$, so

\[\frac{415}{93} = [4; 2, 6, 7],\]

with convergents $4$, $9/2$, $58/13$ and $415/93$.

The algorithm works in any linearly ordered field with a floor function. Its head term is the floor of $v$, its partial numerators are all equal to $1$, and its partial denominators are integers that are at least $1$, so the result is a regular continued fraction.

Examples

The golden ratio. $\varphi = (1 + \sqrt 5)/2$ satisfies $\varphi = 1 + 1/\varphi$, so $\varphi = [1; 1, 1, 1, \dots]$. Its convergents are $1, 2, 3/2, 5/3, 8/5, \dots$, quotients of consecutive Fibonacci numbers.
The square root of two. Since $1/(\sqrt 2 - 1) = \sqrt 2 + 1 = 2 + (\sqrt 2 - 1)$, one gets $\sqrt 2 = [1; 2, 2, 2, \dots]$, with convergents $1, 3/2, 7/5, 17/12, 41/29, \dots$. Their numerators and denominators satisfy $p_n^2 - 2 q_n^2 = \pm 1$, which links the expansion to Pell's equation.

Properties

Let $v$ lie in a linearly ordered field with a floor function, such as the real numbers, and let $p_n/q_n$ be the convergents of its expansion.

Termination. The expansion of $v$ terminates if and only if $v$ is rational. If the expansion has no term $a_{n+1}$, then the $n$-th convergent equals $v$.
Determinant formula. For a simple continued fraction with terms in any field, whenever the term $a_{n+1}$ exists, $p_n q_{n+1} - q_n p_{n+1} = (-1)^{n+1}$. With integer terms this shows that $p_n$ and $q_n$ are coprime, so each convergent is in lowest terms.
Growth of denominators. Whenever the expansion has a term $a_n$, the denominator $q_n$ is at least the Fibonacci number $F_{n+1}$, with $F_0 = 0$ and $F_1 = 1$; the golden ratio shows that this bound is attained.
Error bound. Whenever the expansion has a term $a_{n+1}$, $|v - p_n/q_n| \le 1/(q_n q_{n+1})$. Since the denominators never decrease, this is at most $1/q_n^2$.
Convergence. When the field carries its order topology, the convergents tend to $v$.
Legendre's theorem. If $v$ is real and a rational number $x/y$ in lowest terms with $y \ge 1$ satisfies $|v - x/y| < 1/(2y^2)$, then $x/y$ is one of the convergents of $v$.

Among classical regular continued fractions, every irrational real number has exactly one infinite expansion, and every infinite one converges to an irrational number. A rational number has exactly two finite expansions, related by $[a_0; a_1, \dots, a_n] = [a_0; a_1, \dots, a_n - 1, 1]$ where $a_n \ge 2$ or $n = 0$, such as $[4; 2, 6, 7] = [4; 2, 6, 6, 1]$ or $[1] = [0; 1]$. A real number has an eventually periodic expansion if and only if it is an irrational root of a quadratic polynomial with integer coefficients.

For $n \ge 1$ the denominators strictly increase, so for an irrational real number $v$ the error bound gives infinitely many rationals $x/y$ with $|v - x/y| < 1/y^2$, an explicit form of Dirichlet's approximation theorem. Generalized continued fractions with arbitrary partial numerators appear in analysis as expansions of functions, and for a positive integer $d$ that is not a square, the periodic expansion of $\sqrt d$ yields the fundamental solution of Pell's equation $x^2 - d y^2 = 1$.

In Mathlib

Mathlib builds the three notions as successive restrictions: a generalized continued fraction over any type, the simple ones among them, and the regular ones among those. A regular continued fraction only asks for positive partial denominators, not for integers; integrality is a property of the expansion of a number, proved separately. The head term is stored apart, so Mathlib's partial denominators $d_0, d_1, \dots$ are the classical $a_1, a_2, \dots$, and a finite continued fraction is a sequence that terminates. Convergents are defined for every index $n$ and take values in the field (more generally, division ring) of the terms; once a continued fraction has no term $a_{n+1}$, every later convergent equals the $n$-th. For real numbers there is also a direct recursive definition of the convergents as rational numbers, which agrees with the general one.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibContFract

Uses 5

Statement usesInteger · Rational number · Real number · Sequence · Field

StructureReal number #

The real numbers are the numbers used to measure continuous quantities such as length, time and mass; together they make up the real line $\mathbb{R}$. They extend the rational numbers by filling the gaps between them, so that quantities such as $\sqrt 2$ and $\pi$ have a place on the line. Algebraically they form an ordered field, and what sets them apart is completeness: every nonempty set of real numbers that is bounded above has a least upper bound. Completeness is what makes limits, continuity, derivatives and integrals behave well, and nearly all of analysis takes place over $\mathbb{R}$ or over spaces built from it.

Definition

There are several equivalent ways to build $\mathbb{R}$ from $\mathbb{Q}$. The construction by Cauchy sequences runs as follows. A sequence $(q_n)$ of rational numbers is a Cauchy sequence if its terms eventually stay arbitrarily close to one another: for every rational $\varepsilon > 0$ there is an index $N$ with $|q_m - q_n| < \varepsilon$ for all $m, n \ge N$. Two Cauchy sequences $(p_n)$ and $(q_n)$ are called equivalent if $p_n - q_n$ tends to $0$. A real number is an equivalence class of Cauchy sequences of rationals; this is how Mathlib defines the real numbers, and two Cauchy sequences give the same real number exactly when they are equivalent. A rational number $q$ is identified with the class of the constant sequence $q, q, q, \dots$

Sums and products of classes are computed term by term. A class is positive when its sequences are eventually at least some fixed positive rational, and $x < y$ means that $y - x$ is positive. A Cauchy sequence that does not tend to $0$ is eventually bounded away from $0$, so its terms can be inverted from some point on; this gives inverses of nonzero classes, and with these operations $\mathbb{R}$ is a field (see the field of real numbers).

Other constructions use Dedekind cuts (splittings of $\mathbb{Q}$ into a nonempty lower part with no greatest element and a nonempty upper part lying entirely above it) or infinite decimal expansions. One can also take $\mathbb{R}$ to be any complete ordered field; the section on uniqueness below explains why all these approaches give the same structure.

Examples

Every natural number, integer and rational number is a real number.
A real number is a square exactly when it is nonnegative. In particular $2$ has a square root, and $\sqrt 2$ is irrational, that is, not equal to any rational number (see the irrationality of the square root of 2).
The circle constant $\pi$ is also irrational.
The rationals form a countable set, while the set of real numbers has the cardinality of the continuum, $2^{\aleph_0}$, and so is not countable (see the non-denumerability of the continuum). In particular the irrational numbers far outnumber the rational ones.

Properties

Ordered field. The order on $\mathbb{R}$ is total (see order), and it is compatible with the field operations: adding the same number to both sides of an inequality preserves it, $0 < 1$, and multiplying both sides of a strict inequality by a positive number preserves it.
Least upper bounds. Every nonempty set of real numbers that is bounded above has a least upper bound, its supremum. This fails in $\mathbb{Q}$: the rationals $q$ with $q^2 < 2$ have no rational least upper bound.
Cauchy completeness. Every Cauchy sequence of real numbers converges to a real number. With the distance $d(x, y) = |x - y|$, $\mathbb{R}$ is therefore a complete metric space (see the metric structure on $\mathbb{R}$).
Archimedean property. For every real $x$ and every real $y > 0$, some natural multiple $ny$ is at least $x$. In particular no real number exceeds every natural number.
Density of the rationals. If $x < y$ are real numbers, there is a rational $q$ with $x < q < y$; Mathlib proves this for every Archimedean ordered field.
Rigidity. Every ring homomorphism from $\mathbb{R}$ to itself is the identity. Such a map sends squares to squares, hence preserves the order, and it fixes every rational number, so density of the rationals forces it to fix everything.

Completeness is the source of the basic theorems of real analysis, among them the Bolzano–Weierstrass theorem and the intermediate value theorem.

Uniqueness

An ordered field is complete if every nonempty subset that is bounded above has a least upper bound. The real numbers are, up to isomorphism, the only complete ordered field: for any two complete ordered fields there is an isomorphism between them that preserves addition, multiplication and order, and such an isomorphism is unique. Along the way one shows that every complete ordered field is Archimedean. So any construction of $\mathbb{R}$ that yields a complete ordered field gives the same object, and results about $\mathbb{R}$ do not depend on the construction chosen.

The complex numbers are obtained from $\mathbb{R}$ by adjoining a square root of $-1$.
The extended real numbers add the two points $+\infty$ and $-\infty$.
The $p$-adic numbers arise by completing $\mathbb{Q}$ with respect to the $p$-adic absolute value instead of the usual one.
The hyperreal numbers form an ordered field extending $\mathbb{R}$ that is not Archimedean and contains infinitesimals.
More generally, $\mathbb{R}$ is the completion of $\mathbb{Q}$ with its usual distance.

In Mathlib

Mathlib defines the real numbers as a structure wrapping the completion of $\mathbb{Q}$ with respect to the absolute value, using the same general Cauchy-sequence completion that also produces the $p$-adic numbers. Its Cauchy condition compares each later term with a fixed earlier one, which is equivalent to the usual one. The construction is used only to set up the field, order and completeness; later results rely on those properties rather than on representing sequences. Equality and order of real numbers are not computable, so they are decided by classical logic. Operations are made total by convention: the inverse of $0$ is $0$ (stated for every group with zero), so division by $0$ gives $0$; the supremum of the empty set is $0$, as is the supremum of a set that is not bounded above; and the square root of $x$ is $0$ exactly when $x \le 0$. The least upper bound property appears as the statement that $\mathbb{R}$ is a conditionally complete linear order, and the uniqueness theorem is stated for arbitrary conditionally complete linearly ordered fields.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibReal

Uses 3 · Used by 29

Statement usesRational number · Field · Cauchy sequence

Used byLiouville’s Theorem and the Construction of Transcendental Numbers · The Non-Denumerability of the Continuum · Arithmetic Mean/Geometric Mean · Divergence of the Harmonic Series · Sum of a Geometric Series · Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) · Positive measure · Ruzsa covering lemma · Small tripling implies small powers · Solutions to Pell's equation (Number theory) · Complex number · Continued fraction · Extended real number · Hyper-real number · Liouville's theorem on existence of transcendental numbers · Almost sure convergence · Discrete law · Hausdorff distance · Hölder continuity · Lipschitz continuity · Carathéodory's theorem (measure theory) · M. Riesz extension theorem · Hahn embedding theorem · Sylvester's law of inertia (existence) · Approximation by step functions · Borel-Cantelli lemma (easy direction) · Field $\R$ of real numbers · Order · Uniform convergence norm (sup-norm)

DefinitionExtended real number #

The extended real numbers are the real numbers together with two further elements, $+\infty$ and $-\infty$, placed above and below every real number. The resulting set, written $\overline{\mathbb{R}}$ or $[-\infty, +\infty]$, is the set of extended real numbers. Adjoining the two infinities makes the order complete: every subset acquires a supremum and an infimum. This makes the extended reals a natural home for suprema, infima, limits superior and inferior and limits of unbounded sequences, and, in their nonnegative part, for measures and integrals of nonnegative functions.

Definition

As a set, $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, +\infty\}$. The order extends that of $\mathbb{R}$ by declaring $-\infty < x < +\infty$ for every real $x$: indeed $-\infty$ lies below every real number and $+\infty$ lies above every real number. The real line sits inside unchanged: for real $x$ and $y$, $x < y$ holds in $\overline{\mathbb{R}}$ exactly when it holds in $\mathbb{R}$, and the real numbers are precisely the elements strictly between $-\infty$ and $+\infty$.

With this order $\overline{\mathbb{R}}$ is a complete linear order, with least element $-\infty$ and greatest element $+\infty$. A subset that is unbounded above in $\mathbb{R}$ has supremum $+\infty$, and the empty set has supremum $-\infty$ and infimum $+\infty$.

Arithmetic

Negation extends to an order-reversing involution, with $-(+\infty) = -\infty$, $-(-\infty) = +\infty$, and $-a \le -b$ if and only if $b \le a$, so that negation is an order isomorphism from $\overline{\mathbb{R}}$ to its order dual.

Addition extends the real sum by $+\infty + x = +\infty$ for every $x \neq -\infty$. The sum $(+\infty) + (-\infty)$ has no natural value, and conventions differ. One common choice, used in Mathlib, sets $-\infty + x = -\infty$ for every $x$, including $x = +\infty$. Consequently subtraction, defined by $a - b = a + (-b)$, gives $x - (+\infty) = -\infty$ for every $x$, and while $x - x = 0$ for real $x$, the differences $(+\infty) - (+\infty)$ and $(-\infty) - (-\infty)$ both equal $-\infty$. The extended reals therefore form a commutative monoid under addition but not a group. Strict inequalities still add: if $a < b$ and $c < d$, then $a + c < b + d$.

Multiplication follows the rule of signs: $x \cdot (+\infty) = +\infty$ for $x > 0$, $x \cdot (+\infty) = -\infty$ for $x < 0$, and $(-\infty)(-\infty) = +\infty$. The convention $0 \cdot x = 0$ for every extended real $x$ settles the remaining case. Multiplication is commutative and associative, but it does not distribute over addition in general:

\[(1 + (-1)) \cdot (+\infty) = 0, \qquad 1 \cdot (+\infty) + (-1) \cdot (+\infty) = -\infty.\]

Distributivity holds in two useful cases: $x(y + z) = xy + xz$ whenever $x$ is real and nonnegative, and $c(a + b) = ca + cb$ whenever $a, b \ge 0$.

Topology

The extended reals carry the order topology, in which the neighbourhoods of $+\infty$ are the sets containing a ray $(r, +\infty]$ with $r$ real. The inclusion of $\mathbb{R}$ is a homeomorphism onto an open subset, and the finite elements form a space homeomorphic to $\mathbb{R}$. Since $\overline{\mathbb{R}}$ is a complete linear order, it is compact; it is homeomorphic to the closed interval $[-1, 1]$, so it is a two-point compactification of the real line. The rationals are dense: between any two extended reals $a < b$ there is a rational number.

Convergence to the infinities matches the familiar notion: a sequence tends to $+\infty$ in $\overline{\mathbb{R}}$ exactly when, for every real $r$, its terms eventually exceed $r$, and for real-valued sequences this is the usual divergence to $+\infty$. Addition is continuous at every pair other than $(+\infty, -\infty)$ and $(-\infty, +\infty)$, where no convention could make it continuous: near $(+\infty, -\infty)$ the sums $n + (c - n)$, with $n$ large, take every real value $c$.

The nonnegative extended reals, in which measures and integrals of nonnegative functions take their values, can be identified with the closed interval $[0, +\infty]$ of $\overline{\mathbb{R}}$.
The exponential extends with $e^{-\infty} = 0$ and $e^{+\infty} = +\infty$ to a homeomorphism from $\overline{\mathbb{R}}$ onto $[0, +\infty]$. With the convention $0 \cdot \infty = 0$ on $[0, +\infty]$, it satisfies $e^{x + y} = e^x e^y$ for all extended reals $x$ and $y$; the choice $-\infty + (+\infty) = -\infty$ is what makes this hold without exception.
The projectively extended real line adds a single point $\infty$ instead of two; topologically it is a circle rather than a closed interval.
The hyperreal numbers also contain infinite elements, but they form an ordered field with infinitesimals; the extended reals contain no infinitesimals and are not a field.

In Mathlib

Mathlib builds the extended reals by adjoining a top element to $\mathbb{R}$ and then a bottom element to the result. Its order, lattice structure and addition come from this construction, which is why the sum of $+\infty$ and $-\infty$ is $-\infty$: the bottom element absorbs everything under addition. Completeness of the order is inherited from a general fact about conditionally complete linear orders, and the topology is defined as the order topology. Multiplication is defined by cases, with $0$ times anything equal to $0$. Mathlib also defines a reciprocal $x \mapsto x^{-1}$, which agrees with the real reciprocal on nonzero reals and sends $\pm\infty$ and $0$ to $0$ (of $+\infty$, of $-\infty$, of $0$). Passing back to the reals, the map to $\mathbb{R}$ sends $+\infty$ to $0$, sends $-\infty$ to $0$, and is the identity on real numbers. The nonnegative extended reals, used throughout measure theory, are a separate type that Mathlib maps into the extended reals.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibEReal

Uses 1 · Used by 3

Statement usesReal number

Used byFundamental Theorem of Integral Calculus · Dirichlet’s Theorem · Fundamental theorem of calculus, part 2

StructureComplex number #

A complex number is an expression $a + bi$ in which $a$ and $b$ are real numbers and $i$ is a number whose square is $-1$. The complex numbers form a field, written $\mathbb{C}$, that contains the real numbers and in which every nonconstant polynomial equation has a solution. This makes $\mathbb{C}$ the natural setting for algebra, for the theory of analytic functions, and for much of number theory, geometry and physics.

Definition

A complex number is an ordered pair $z = (a, b)$ of real numbers, called its real part $a = \operatorname{Re} z$ and its imaginary part $b = \operatorname{Im} z$. Two complex numbers are equal when their real parts agree and their imaginary parts agree. Addition is componentwise, and multiplication is defined by

\[(a, b)(c, d) = (ac - bd,\ ad + bc).\]

The real part of a product is $ac - bd$ and its imaginary part is $ad + bc$. A real number $r$ is identified with the pair $(r, 0)$; this identification is injective and respects addition and multiplication, so $\mathbb{R}$ sits inside $\mathbb{C}$. The imaginary unit is $i = (0, 1)$, and the multiplication rule gives $i^2 = -1$. Every complex number can then be written as $z = a + bi$ with $a = \operatorname{Re} z$ and $b = \operatorname{Im} z$, and products are computed by expanding and replacing $i^2$ by $-1$.

With these operations $\mathbb{C}$ is a field (see the field of complex numbers). The inverse of a nonzero $z = a + bi$ is

\[z^{-1} = \frac{a - bi}{a^2 + b^2}.\]

Conjugate and absolute value

The complex conjugate of $z = a + bi$ is $\bar z = a - bi$: it has the same real part and the negated imaginary part. Conjugation preserves sums and products, and $\bar z = z$ exactly when $z$ is real. The product of a number and its conjugate is the real number $z \bar z = a^2 + b^2$, which is positive unless $z = 0$.

The absolute value (or modulus) $|z|$ is the nonnegative square root of $a^2 + b^2$, so that $|z|^2 = a^2 + b^2$. It is the distance from $0$ to the point $(a, b)$ in the plane. It is multiplicative, $|zw| = |z|\,|w|$, and satisfies the triangle inequality $|z + w| \le |z| + |w|$. The distance $|z - w|$ makes $\mathbb{C}$ a complete metric space, isometric to the Euclidean plane.

Examples

$(1 + 2i)(3 - i) = 3 - i + 6i - 2i^2 = 5 + 5i$.
$\dfrac{1}{1 + i} = \dfrac{1 - i}{2}$, since $(1 + i)(1 - i) = 2$.
The equation $z^2 = -1$ has the two solutions $i$ and $-i$, and $|i| = 1$.
$|3 + 4i| = 5$, so multiplying by $3 + 4i$ scales lengths in the plane by $5$.

Properties

Dimension over the reals. As a vector space over $\mathbb{R}$, $\mathbb{C}$ has basis $1, i$, so its dimension is $2$.
Algebraic closure. By the fundamental theorem of algebra, every polynomial of positive degree with complex coefficients has a complex root; equivalently, $\mathbb{C}$ is algebraically closed (see algebraically closed field). Every nonconstant complex polynomial therefore factors as a constant times a product of linear factors.
Characteristic zero. $\mathbb{C}$ has characteristic zero (see characteristic zero), since it contains $\mathbb{R}$.
No field ordering. In any ordered field squares are nonnegative, so $1 = 1^2 > 0$ and $-1 = i^2 \ge 0$ would contradict each other. Hence $\mathbb{C}$ admits no ordering compatible with its field operations.
Automorphisms. The only ring homomorphisms from $\mathbb{C}$ to itself that fix every real number, that is, the $\mathbb{R}$-algebra homomorphisms, are the identity and conjugation. The same two maps are the only continuous ring homomorphisms from $\mathbb{C}$ to itself.

Polar form and the exponential

The complex exponential satisfies $e^{z + w} = e^z e^w$ for all complex $z$ and $w$ and Euler's formula $e^{ix} = \cos x + i \sin x$ for every complex $x$. For real $x$ the number $e^{ix}$ has absolute value $1$, and taking $x = \pi$ gives $e^{i\pi} = -1$.

Every complex number has a polar form $z = |z|\,e^{i \arg z}$, where the argument $\arg z$ of a nonzero $z$ is the angle, taken in $(-\pi, \pi]$, from the positive real axis to the point $z$. For $z = 0$ there is no such angle; the argument is taken to be $0$, and the polar form holds trivially. In polar form multiplication multiplies absolute values and adds arguments up to a multiple of $2\pi$, so for real $x$ raising $\cos x + i \sin x$ to the $n$-th power multiplies its argument by $n$. Combining Euler's formula with the addition law for the exponential, $(\cos x + i \sin x)^n = (e^{ix})^n = e^{inx}$, gives De Moivre's formula $(\cos x + i \sin x)^n = \cos nx + i \sin nx$ for every complex $x$ and natural number $n$. For $n \ge 1$ the $n$-th roots of unity are the numbers $e^{2\pi i k/n}$ with $0 \le k < n$, and there are exactly $n$ of them.

The complex numbers are the degree-$2$ extension of $\mathbb{R}$ obtained by adjoining a root of $x^2 + 1$. Applying the same pair construction to complex numbers, with a suitably twisted multiplication, gives the quaternions, a noncommutative division ring of dimension $4$ over $\mathbb{R}$. Complex inner product spaces and the complex sine and cosine functions are built on $\mathbb{C}$, and analysis of functions of a complex variable is the subject of complex analysis.

In Mathlib

Mathlib defines a complex number as a structure with two real fields, its real and imaginary parts, and builds the field operations on top of this pair. The real numbers enter through a coercion that sends $r$ to $(r, 0)$. Division follows Mathlib's general convention that the inverse of $0$ is $0$, so the formula $z^{-1} = \bar z / (a^2 + b^2)$ holds for every $z$, zero included. The absolute value is the norm of $\mathbb{C}$, and the squared modulus $a^2 + b^2$ is also available as a separate function, defined as $(\operatorname{Re} z)^2 + (\operatorname{Im} z)^2$, that is multiplicative and avoids square roots. Conjugation is the star operation of $\mathbb{C}$ as a star ring. Mathlib also provides a partial order on $\mathbb{C}$, in which $z \le w$ means that $w - z$ is a nonnegative real number; it is available only on request and is not a field ordering, since numbers with different imaginary parts are incomparable.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibComplex

Uses 2 · Used by 28

Statement usesReal number · Field

Definition$p$-adic number #

For a prime number $p$, the $p$-adic numbers form a field $\mathbb{Q}_p$ that contains the rational numbers and is complete for a notion of size in which a number is small when it is divisible by a high power of $p$. Just as the real numbers arise by filling in the gaps of $\mathbb{Q}$ for the ordinary absolute value, $\mathbb{Q}_p$ arises by filling them in for the $p$-adic absolute value. The $p$-adic numbers let analytic methods (limits, series, approximation) be applied to questions about divisibility and congruences, and they are a basic tool of modern number theory.

Definition

Every nonzero rational number $x$ can be written as $x = p^{v} a/b$ with $v$ an integer and $a, b$ integers not divisible by $p$. The exponent $v$ is determined by $x$; it is the $p$-adic valuation $v_p(x)$, the multiplicity of $p$ in the numerator minus its multiplicity in the denominator. The $p$-adic absolute value of $x$ is

\[|x|_p = p^{-v_p(x)}, \qquad |0|_p = 0.\]

It satisfies $|xy|_p = |x|_p\,|y|_p$ and the strong triangle inequality $|x + y|_p \le \max(|x|_p, |y|_p)$, so $d(x, y) = |x - y|_p$ is a metric on $\mathbb{Q}$. This metric space is not complete. The field $\mathbb{Q}_p$ is its completion: its elements are equivalence classes of Cauchy sequences of rationals for $|\cdot|_p$, two sequences being equivalent when their difference tends to $0$. Sums and products are taken term by term.

Examples

Since $18 = 2 \cdot 3^2$, one has $|18|_3 = 1/9$, while $|1/6|_3 = 3$. In $\mathbb{Q}_3$ the integer $18$ is close to $0$ and the fraction $1/6$ is large.
The prime itself has $|p|_p = 1/p$, and $|p^n|_p = p^{-n}$ for every natural number $n$, so the powers $p^n$ tend to $0$ in $\mathbb{Q}_p$.
Every integer $k$ satisfies $|k|_p \le 1$, with $|k|_p < 1$ if and only if $p$ divides $k$.
Because $|p^n|_p \to 0$, the geometric series $1 + p + p^2 + \cdots$ converges in $\mathbb{Q}_p$ to $1/(1 - p)$. Multiplying by $p - 1$ gives $$-1 = (p - 1) + (p - 1)p + (p - 1)p^2 + \cdots,$$ a series with digits between $0$ and $p - 1$ that converges to the rational number $-1$.
More generally, every nonzero $x \in \mathbb{Q}_p$ has a unique expansion $x = \sum_{n \ge m} a_n p^n$ with an integer $m$, digits $a_n \in \{0, 1, \dots, p - 1\}$ and $a_m \neq 0$; the sum may have infinitely many nonzero terms, but only finitely many negative powers of $p$ occur.

Properties

Field and norm. The absolute value extends from $\mathbb{Q}$ to $\mathbb{Q}_p$; the extended norm restricts to $|\cdot|_p$ on the rationals, and with it $\mathbb{Q}_p$ is a normed field.
Completeness and density. Every Cauchy sequence in $\mathbb{Q}_p$ converges, and the rationals are dense in $\mathbb{Q}_p$.
Ultrametric inequality. For all $x, y \in \mathbb{Q}_p$, $|x + y|_p \le \max(|x|_p, |y|_p)$, and equality holds when $|x|_p \neq |y|_p$. Consequently every triangle is isosceles, and, since $\mathbb{Q}_p$ is complete, a series in $\mathbb{Q}_p$ converges exactly when its terms tend to $0$.
Valuation. The valuation extends to $\mathbb{Q}_p$: it agrees with $v_p$ on rationals, $|x|_p = p^{-v_p(x)}$ for $x \neq 0$, and $v_p(xy) = v_p(x) + v_p(y)$ for nonzero $x$ and $y$. The norm therefore takes only the values $0$ and $p^n$ for $n \in \mathbb{Z}$, and every nonzero $x$ is $p^{v_p(x)}u$ with $|u|_p = 1$.
Integers. The closed unit ball $\{x : |x|_p \le 1\}$ is a subring, the $p$-adic integers $\mathbb{Z}_p$. It is compact, its units are exactly the elements of norm $1$, it is a local ring whose maximal ideal is generated by $p$, and $\mathbb{Q}_p$ is its field of fractions. Since $\mathbb{Z}_p$ is a compact neighbourhood of $0$, the field $\mathbb{Q}_p$ is locally compact.

Ostrowski's theorem explains why the $p$-adic fields and $\mathbb{R}$ are the natural completions of $\mathbb{Q}$: every nontrivial real-valued absolute value on $\mathbb{Q}$ is equivalent either to the ordinary absolute value or to the $p$-adic absolute value for exactly one prime $p$.
Hensel's lemma turns approximate roots into exact ones: for a polynomial $F$ with coefficients in $\mathbb{Z}_p$ and $a \in \mathbb{Z}_p$ with $|F(a)|_p < |F'(a)|_p^2$, there is a unique root $z \in \mathbb{Z}_p$ of $F$ with $|z - a|_p < |F'(a)|_p$. For example, $a = 2$ and $F = X^2 + 1$ give $|F(2)|_5 = 1/5 < 1 = |F'(2)|_5^2$, so $-1$ has a square root in $\mathbb{Q}_5$.
The construction is a special case of the completion of a metric space, and the same recipe applied to the ordinary absolute value produces $\mathbb{R}$.

In Mathlib

Mathlib takes $p$ to be a natural number together with a standing hypothesis that it is prime. It builds $\mathbb{Q}_p$ with the same concrete construction by Cauchy sequences of rationals that it uses for the real numbers, rather than through its general completion of uniform spaces, and the field structure is inherited from that construction. The main norm is real-valued, so that $\mathbb{Q}_p$ fits the general theory of normed fields; a rational-valued version is kept alongside it. The valuation on $\mathbb{Q}_p$ is an integer-valued function that, by convention, assigns $0$ to the number $0$, so statements about it carry nonzero hypotheses; Mathlib also provides an additive valuation with values in the integers extended by $+\infty$, which sends $0$ to $+\infty$ as in the textbook convention. The $p$-adic integers are defined as the subring of elements of norm at most $1$, not as an inverse limit of the rings $\mathbb{Z}/p^n\mathbb{Z}$.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibPadic

Uses 6 · Used by 1

Statement usesRational number · Prime numbers · Field · Metric space · Cauchy sequence · Completion

Used by$p$-adic integer

Definition$p$-adic integer #

For a prime number $p$, the $p$-adic integers form the ring $\mathbb{Z}_p$ of $p$-adic numbers whose $p$-adic absolute value is at most $1$. They play for the field $\mathbb{Q}_p$ the role that the integers play for the rational numbers, and they encode, in a single ring, all the congruences modulo $p, p^2, p^3, \dots$ at once. This makes $\mathbb{Z}_p$ a basic tool of number theory: a problem about solving a congruence modulo every power of $p$ becomes a problem about solving an equation in $\mathbb{Z}_p$, where analytic methods such as Newton's iteration are available.

Definition

Fix a prime $p$. Every nonzero $p$-adic number $x$ has a valuation $v(x) \in \mathbb{Z}$, and its absolute value is $|x|_p = p^{-v(x)}$, with $|0|_p = 0$. The ring of $p$-adic integers is

\[\mathbb{Z}_p = \{\, x \in \mathbb{Q}_p : |x|_p \le 1 \,\},\]

the closed unit ball of $\mathbb{Q}_p$ (the definition). The ultrametric inequality $|x + y|_p \le \max(|x|_p, |y|_p)$ shows that this set is closed under addition, and multiplicativity of the absolute value shows it is closed under multiplication; it contains $0$ and $1$ and, since $|-x|_p = |x|_p$, is closed under negation, so $\mathbb{Z}_p$ is a subring of $\mathbb{Q}_p$.

Two other descriptions give the same ring. Up to isomorphism, $\mathbb{Z}_p$ is the completion of $\mathbb{Z}$ for the metric $d(a, b) = |a - b|_p$, in which integers are close when their difference is divisible by a high power of $p$. It is also the inverse limit of the rings $\mathbb{Z}/p^n\mathbb{Z}$: a $p$-adic integer amounts to a sequence of residues $x_n \in \mathbb{Z}/p^n\mathbb{Z}$, each reducing to the previous one modulo $p^{n-1}$. Concretely, every $p$-adic integer has a unique expansion

\[x = a_0 + a_1 p + a_2 p^2 + \cdots, \qquad 0 \le a_i \le p - 1,\]

which converges because $|p^n|_p = p^{-n}$ tends to $0$.

Examples

Every integer is a $p$-adic integer, and an integer $k$ has absolute value less than $1$ exactly when $p$ divides $k$.
More generally, a rational number whose denominator in lowest terms is not divisible by $p$ has $p$-adic absolute value at most $1$, so it lies in $\mathbb{Z}_p$; conversely, a rational number whose reduced denominator is divisible by $p$ does not. For instance $1/2 \in \mathbb{Z}_3$ but $1/3 \notin \mathbb{Z}_3$.
The geometric series gives $1 + p + p^2 + \cdots = 1/(1 - p)$, and the expansion of $-1$ is $(p - 1) + (p - 1)p + (p - 1)p^2 + \cdots$, since its partial sums are $p^n - 1$.
In $\mathbb{Z}_5$ there is a square root of $-1$: the congruence $x^2 \equiv -1$ has the solution $x \equiv 2 \pmod 5$, and Hensel's lemma (below) lifts it to an element of $\mathbb{Z}_5$ whose expansion begins $2 + 1 \cdot 5 + 2 \cdot 5^2 + \cdots$.

Properties

Units and factorization. For $x \in \mathbb{Z}_p$, $x$ is a unit exactly when $|x|_p = 1$, and it is a non-unit exactly when $|x|_p < 1$. Every nonzero $x$ has $|x|_p = p^{-v(x)}$ for a natural number $v(x)$, and it can be written as $x = u\,p^{v(x)}$ with $u$ a unit. The valuation is additive on nonzero elements: $v(xy) = v(x) + v(y)$.

Ideals. $\mathbb{Z}_p$ is an integral domain of characteristic zero. It is a local ring: its unique maximal ideal is the ideal generated by $p$, and $p$ is a prime element of $\mathbb{Z}_p$. Every ideal is principal; in fact every nonzero ideal equals $p^n \mathbb{Z}_p$ for some $n \ge 0$. Thus $\mathbb{Z}_p$ is a discrete valuation ring, that is, a local principal ideal domain that is not a field, and its field of fractions is $\mathbb{Q}_p$.

Reduction modulo powers of $p$. For each $n$ there is a ring homomorphism $\mathbb{Z}_p \to \mathbb{Z}/p^n\mathbb{Z}$ that sends $x$ to the residue of the truncation $a_0 + a_1 p + \cdots + a_{n-1}p^{n-1}$, and its kernel is $p^n \mathbb{Z}_p$. In particular the residue field, the quotient of $\mathbb{Z}_p$ by its maximal ideal $p\mathbb{Z}_p$, is isomorphic to $\mathbb{Z}/p\mathbb{Z}$. Two $p$-adic integers are equal if their reductions modulo $p^n$ agree for every $n$. The inverse-limit description is the following universal property: given a ring $R$ and ring homomorphisms $f_n \colon R \to \mathbb{Z}/p^n\mathbb{Z}$ compatible with reduction, there is a ring homomorphism $R \to \mathbb{Z}_p$ whose reduction modulo $p^n$ is $f_n$ for every $n$, and it is the only such homomorphism.

Topology. The absolute value makes $\mathbb{Z}_p$ a metric space satisfying the ultrametric inequality. It is complete (see completeness) and compact, and the integers are dense in it. Each ideal $p^n\mathbb{Z}_p$ is both open and closed, and the ring is totally disconnected.

Hensel's lemma. Let $F$ be a polynomial with coefficients in $\mathbb{Z}_p$ and $a \in \mathbb{Z}_p$ with $|F(a)|_p < |F'(a)|_p^2$. Then there is a unique root $z$ of $F$ with $|z - a|_p < |F'(a)|_p$, and it satisfies $|F'(z)|_p = |F'(a)|_p$. When $|F'(a)|_p = 1$, this says that a simple root of $F$ modulo $p$ lifts to a root in $\mathbb{Z}_p$.

The field $\mathbb{Q}_p$ of $p$-adic numbers is obtained from $\mathbb{Z}_p$ by inverting $p$. Continuous functions on $\mathbb{Z}_p$ are described by Mahler's theorem, which expands them in binomial coefficients. The ring of Witt vectors of the field with $p$ elements is isomorphic to $\mathbb{Z}_p$, and the Witt vector construction generalizes $\mathbb{Z}_p$ to other perfect fields of characteristic $p$. The ring of integers of a finite extension of $\mathbb{Q}_p$ is again a complete discrete valuation ring and shares most of the properties above.

In Mathlib

Mathlib defines the $p$-adic integers for a natural number $p$ together with the hypothesis that $p$ is prime, passed as a typeclass argument so that instance search can find it once it is in scope; outside a few small explicit primes, the user puts that fact in scope by hand. The ring is the subtype of the $p$-adic numbers of norm at most $1$, with the ring operations inherited from the subring, so membership is a property of a $p$-adic number rather than a separate construction. The norm is real-valued and normalized so that $p$ has norm $1/p$. The valuation of a $p$-adic integer is a natural number, and by convention the valuation of $0$ is $0$ rather than infinity, which is why statements about the valuation carry nonzero hypotheses. The inverse-limit description is not the definition but a theorem, phrased as the universal property above, and the local, discrete valuation ring, domain and compactness properties are recorded as typeclass instances.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibPadicInt

Uses 4 · Used by 2

Statement uses$p$-adic number · Prime numbers · Subring · Integer

Used byHensel's lemma (for $\mathbb{Z}_p$) · Mahler's theorem

DefinitionHyper-real number #

The hyper-real numbers, or hyperreals, form an ordered field $^*\mathbb R$ that contains the real numbers together with positive infinitesimals, numbers greater than $0$ but smaller than every positive real, and infinite elements, numbers larger than every real. They are the number system of nonstandard analysis. In $^*\mathbb R$ a derivative can be computed from a quotient of infinitesimal changes and a limit can be found by rounding a hyper-real number to the nearest real, which makes arguments with infinitesimals rigorous.

Definition

The usual construction is an ultrapower of $\mathbb R$. An ultrafilter on the natural numbers is a filter $\mathcal U$ of subsets of $\mathbb N$, not containing the empty set, such that for every $A \subseteq \mathbb N$ either $A$ or its complement belongs to $\mathcal U$. It is nonprincipal if it contains no finite set, or equivalently every set with finite complement. Nonprincipal ultrafilters exist by the axiom of choice; Mathlib fixes one, its hyperfilter, which contains every set with finite complement. A set in $\mathcal U$ is thought of as containing almost all indices.

Two real sequences $(a_n)$ and $(b_n)$ are identified when $\{n : a_n = b_n\} \in \mathcal U$. A hyper-real number is an equivalence class $[a_n]$, and the hyper-real numbers are the set of all such classes: each sequence defines one and every hyper-real number comes from a sequence. Arithmetic is termwise,

\[[a_n] + [b_n] = [a_n + b_n], \qquad [a_n]\,[b_n] = [a_n b_n],\]

and $[a_n] < [b_n]$ exactly when $\{n : a_n < b_n\} \in \mathcal U$. The order is total because the three sets where $a_n < b_n$, $a_n = b_n$ and $a_n > b_n$ partition $\mathbb N$, so exactly one of them lies in $\mathcal U$. If $[a_n] \neq 0$ then $a_n \neq 0$ for almost all $n$, and inverting those terms gives the inverse. With these operations $^*\mathbb R$ is an ordered field.

A real number $r$ is sent to the class of the constant sequence $(r, r, r, \dots)$. This embedding is an order-preserving ring homomorphism, it is injective, and $r < s$ holds in $^*\mathbb R$ exactly when it holds in $\mathbb R$.

Examples

Let $\omega = [0, 1, 2, 3, \dots]$ be the class of the sequence $(n)$. For a real $r$, all but finitely many $n$ satisfy $n > r$, and that set lies in $\mathcal U$, so $r < \omega$ for every real $r$. Its reciprocal $\varepsilon$ is the class of the sequence $(1/n)$; changing finitely many terms never changes a class, so the term at $n = 0$ does not matter. Indeed the reciprocal of $\omega$ is $\varepsilon$, and $\varepsilon$ is positive and smaller than every positive real. Further examples are $\omega + 1$, $\omega^2$ and $[\sqrt n]$, all infinite, and $\varepsilon^2$, an infinitesimal smaller than $\varepsilon$; the numbers $r + \varepsilon$ and $r - \varepsilon$ differ from the real $r$ by an infinitesimal.

Properties

A hyper-real number $x$ is infinitesimal if $|x| < r$ for every positive real $r$ (so $0$ is infinitesimal), finite if $|x| < r$ for some real $r$, and infinite otherwise. Two hyper-real numbers are infinitely close if their difference is infinitesimal. Sums of infinitesimals and products of an infinitesimal with a finite number are infinitesimal, and the reciprocal of a nonzero infinitesimal is infinite.

Not Archimedean. Since $\omega$ exceeds every natural number, $^*\mathbb R$ is not an Archimedean field.
Not complete. The infinitesimals form a nonempty set bounded above by $1$ with no least upper bound. An upper bound $s$ is at least $\varepsilon > 0$; it cannot be infinitesimal, since $2s$ would then be a larger infinitesimal. So $s \ge r$ for some positive real $r$, and then $s/2$ is a smaller upper bound.
Standard part. Every finite $x$ is infinitely close to exactly one real number, its standard part $\operatorname{st}(x)$: for finite $x$ and real $r$, the difference $x - r$ is infinitesimal exactly when $r = \operatorname{st}(x)$. The completeness of $\mathbb R$ supplies it: $\operatorname{st}(x)$ is the supremum of the reals below $x$. For finite $x$ and $y$, $\operatorname{st}(x + y) = \operatorname{st}(x) + \operatorname{st}(y)$ and $\operatorname{st}(xy) = \operatorname{st}(x)\operatorname{st}(y)$, and $\operatorname{st}(r) = r$ for real $r$.
Limits. A sequence tends to $L$ along $\mathcal U$ if, for every neighbourhood $V$ of $L$, the set of $n$ with $a_n \in V$ lies in $\mathcal U$. If $(a_n)$ tends to $L$ along $\mathcal U$, then $\operatorname{st}([a_n]) = L$. Since $\mathcal U$ contains every set with finite complement, this covers every sequence with limit $L$ in the usual sense. Likewise $(a_n)$ tends to $+\infty$ along $\mathcal U$ exactly when $[a_n]$ is positive and infinite.
Continuity. For a real function $f$ that is continuous at the point $r$, if $(a_n)$ tends to $r$ along $\mathcal U$, then $(f(a_n))$ tends to $f(r)$ along $\mathcal U$.
Transfer. Because $^*\mathbb R$ is an ultrapower, Łoś' theorem applies: a first-order sentence holds in an ultraproduct of nonempty structures exactly when the set of indices whose factor satisfies it belongs to the ultrafilter. Every factor here is $\mathbb R$, so a first-order sentence in a language with a symbol for each real function and relation holds in $^*\mathbb R$ exactly when it holds in $\mathbb R$, where each function $f$ is read as its termwise extension $f^*[a_n] = [f(a_n)]$ and each relation $P$ as the set of classes $[a_n]$ with $P(a_n)$ for almost all $n$. For example, a real function $f$ has derivative $L$ at a real $x$ exactly when $(f^*(x + \delta) - f(x))/\delta$ is infinitely close to $L$ for every nonzero infinitesimal $\delta$. Transfer does not reach statements that quantify over arbitrary subsets, which is why completeness fails.

If the continuum hypothesis holds, all nonprincipal ultrafilters on $\mathbb N$ yield isomorphic ordered fields.

The extended real numbers add only $+\infty$ and $-\infty$ to $\mathbb R$ and do not form a field. Infinitesimal and infinite elements make sense in any ordered ring that is not Archimedean, and the Hahn embedding theorem describes ordered groups through the same Archimedean classes that separate these sizes.

In Mathlib

Mathlib builds the hyperreals as germs of real sequences at its hyperfilter, one ultrafilter on $\mathbb N$ extending the cofinite filter chosen by the axiom of choice, so its hyperreals are a single field rather than a family indexed by ultrafilters. The field operations and the linear order come from the general theory of germs, the reals sit inside as constant sequences, and $\omega$ and $\varepsilon$ are provided by name. Infinitesimal and infinite elements and the standard part are not special to the hyperreals: Mathlib treats them in every ordered field through the Archimedean class of an element, ordered so that smaller elements have larger classes; an element is infinitesimal when its class is above that of $1$ and infinite when it is below. The standard part is defined for every element, with value $0$ at infinite elements, so the standard part of $\omega$ is $0$. The sum and product rules above hold in every ordered field, and the uniqueness statement and the supremum formula in every ordered field that receives an order-preserving ring homomorphism from the reals. The transfer principle is not yet formalized for the hyperreals, though Łoś' theorem is available for ultraproducts of first-order structures.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibHyperreal

Uses 4

Statement usesReal number · Field · Ordered ring · Filter

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Numbers

InductiveNatural number#

Definition

Properties

Induction and recursion

Related concepts

In Mathlib

Sources

InductiveInteger#

Definition

Algebraic structure

Order

Divisibility and primes

Related concepts

In Mathlib

Sources

StructureRational number#

Definition

Examples

Properties

Absolute values and completions

In Mathlib

Sources

DefinitionContinued fraction#

Definition

The expansion of a number

Examples

Properties

Related concepts

In Mathlib

Sources

StructureReal number#

Definition

Examples

Properties

Uniqueness

Related concepts

In Mathlib

Sources

DefinitionExtended real number#

Definition

Arithmetic

Topology

Related concepts

In Mathlib

Sources

StructureComplex number#

Definition

Conjugate and absolute value

Examples

Properties

Polar form and the exponential

Related concepts

In Mathlib

Sources

Definition\(p\)-adic number#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

Definition\(p\)-adic integer#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

DefinitionHyper-real number#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

InductiveNatural number #

InductiveInteger #

StructureRational number #

DefinitionContinued fraction #

StructureReal number #

DefinitionExtended real number #

StructureComplex number #

Definition\(p\)-adic number #

Definition\(p\)-adic integer #

DefinitionHyper-real number #