Redirected from "decimal rational numbers".
Contents
Context
Arithmetic
number theory
number
- natural number, integer number, rational number, real number, irrational number, complex number, quaternion, octonion, adic number, cardinal number, ordinal number, surreal number
arithmetic
arithmetic geometry, function field analogy
Arakelov geometry
Algebra
Contents
Idea
A decimal rational number or decimal fraction is a rational number such that the decimal expansion of has finitely many digits.
Definition
As a subset of the rational numbers
A decimal rational number or decimal fraction is a rational number such that there exists and such that .
As the localisation of the integers at 10
The commutative ring of decimal rational numbers is the localization of the integers away from .
As an initial object of a category
For lack of a better name, let us define a set with decimal fractions to be a set with a function , such that
The integer represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal fraction, and the natural number represents the number of digits to the left of the final digit where the decimal separator ought to be placed after in the decimal numeral representation of the decimal fraction. The axiom above is used to state that equivalent decimals are equal: i.e. 1.00 = 1.000 with decimal numeral representations.
A homomorphism of sets with decimal fractions between two decimal fraction algebras and is a function such that
The category of sets with decimal fractions is the category whose objects are sets with decimal fractions and whose morphisms for sets with decimal fractions , are homomorphisms of sets with decimal fractions. The set of decimal fractions, denoted , is defined as the initial object in the category of sets with decimal fractions.
As a higher inductive type
In homotopy type theory, the type of decimal numbers, denoted , could be defined as the higher inductive type generated by:
Properties
Decidability
Proposition
(Decidability of equality)
For every decimal fraction and , or .
Definition
(Inequality)
For every decimal fraction and , there is a proposition called inequality and defined as
Proposition
(Tight apartness relation)
Inequality is a tight apartness relation: For every decimal fraction and , if , then .
Commutative ring structure
Definition
(Addition)
There exists a binary operation called addition defined as
for , , , .
Proposition
(Associativity of addition)
For every decimal fraction , , and , .
Proof
By definition of the set of decimal fractions, there exist numbers , , , , , such that , , and . Thus,
by definition of addition. By the distributive property of multiplication of integers
and by the fact that exponentiation is an -action with respect to multiplication and by the commutative property of addition of natural numbers,
Finally, by the associative property of addition of integers and natural numbers,
Thus, .
Proposition
(Commutativity of addition)
For every decimal fraction and , .
Proof
By definition of the set of decimal fractions, there exist numbers , , , such that and . Thus,
and
by definition of addition. By the commutativity of addition in the integers and the natural numbers,
Thus, .
Definition
(Zero)
There exists an element called zero and defined as .
Proposition
(Zero is a left identity of addition)
For every decimal fraction , .
Proof
By definition of the set of decimal fractions, there exist numbers , such that . Thus,
by definition of addition. By the absorption property of with respect to multiplication in the integers,
by the fact that exponentiation is an -action with respect to multiplication in the integers,
by the fact that 1 is a right identity element with respect to multiplication in the integers,
and by the fact that 0 is a left identity element with respect to addition in the natural numbers,
Thus, .
Proposition
(Zero is a right identity of addition)
For every decimal fraction , .
Proof
By definition of the set of decimal fractions, there exist numbers , such that . Thus,
by definition of addition. By the absorption property of with respect to multiplication in the integers,
by the fact that exponentiation is an -action with respect to multiplication in the integers,
by the fact that 1 is a right identity element with respect to multiplication in the integers,
and by that 0 is a left identity element with respect to addition in the natural numbers,
Thus, .
Definition
(Negation)
There exists a function called negation and defined as
for , .
Proposition
(Negation is a left inverse of addition)
For every decimal fraction , .
Proof
By definition of the set of decimal fractions, there exist numbers , such that . Thus,
by definition of addition. By the fact that multiplication is a bilinear function in the integers,
and by the fact that negation is a left inverse of addition in the integers,
and by definition of equality of decimal fractions, since
this means that
Thus, .
Proposition
(Negation is a right inverse of addition)
For every decimal fraction , .
Proof
By definition of the set of decimal fractions, there exist numbers , such that . Thus,
by definition of addition. By the fact that multiplication is a bilinear function in the integers,
and by the fact that negation is a right inverse of addition in the integers,
and by definition of equality of decimal fractions, since
this means that
Thus, .
Definition
(Subtraction)
There exists a binary operation called subtraction defined as
for , , , .
Proposition
(Abelian group)
The decimal fractions form an abelian group.
Definition
(Multiplication)
There exists a binary operation called multiplication defined as
for , , , .
Proposition
(Left distributivity of multiplication over addition)
For every decimal fraction , , and , .
Proof
By definition of the set of decimal fractions, there exist numbers , , , , , such that , , and . Thus,
by definition of addition and multiplication. By left distributivity of multiplication over addition of integers,
and by associativity of multiplication of integers,
Now we consider the following integer expressions: by the right distributive property of multiplication over addition in integers,
and by the associative property of multiplication in integers,
By the fact that exponentiation is an -action over multiplication on the integers,
and by the associativity and commutativity of addition on the natural numbers,
Thus,
By definition of equality of decimal fractions, since
then
Thus, .
Proposition
(Right distributivity of multiplication over addition)
For every decimal fraction , , and , .
Proof
By definition of the set of decimal fractions, there exist numbers , , , , , such that , , and . Thus,
by definition of addition and multiplication. By right distributivity of multiplication over addition of integers,
and by associativity of multiplication of integers,
and by commutativity of multiplication of integers,
and by associativity of multiplication of integers,
Now we consider the following integer expressions: by the right distributive property of multiplication over addition in integers,
and by the associative property of multiplication in integers,
By the fact that exponentiation is an -action over multiplication on the integers,
and by the associativity and commutativity of addition on the natural numbers,
Thus,
By definition of equality of decimal fractions, since
then
Thus, .
Proposition
(Associativity of multiplication)
For every decimal fraction , , and , .
Proof
By definition of the set of decimal fractions, there exist numbers , , , , , such that , , and . Thus,
by definition of addition. By the associative property of multiplication of integers and addition of natural numbers,
Thus, .
Proposition
(Commutativity of multiplication)
For every decimal fraction and , .
Proof
By definition of the set of decimal fractions, there exist numbers , , , such that and . Thus,
and
by definition of addition. By the commutativity of multiplication in the integers and the commutativity of addition in the natural numbers,
Thus, .
Definition
(One)
There exists an element called one and defined as .
Proposition
(One is a left identity of multiplication)
For every decimal fraction , .
Proof
By definition of the set of decimal fractions, there exist numbers , such that . Thus,
by the fact that 1 is a left identity element with respect to multiplication in the integers,
and by the fact that 0 is a left identity element with respect to addition in the natural numbers,
Thus, .
Proposition
(One is a right identity of multiplication)
For every decimal fraction , .
Proof
By definition of the set of decimal fractions, there exist numbers , such that . Thus,
by the fact that 1 is a right identity element with respect to multiplication in the integers,
and by the fact that 0 is a right identity element with respect to addition in the natural numbers,
Thus, .
Proposition
(Commutative ring)
The decimal fractions form a commutative ring.
Definition
(Exponentiation)
There exists a binary operation called exponentiation defined as
for , , .
Proposition
(10 is a unit)
There is an element such that and
Proposition
(Powers of 10 are isomorphic to the integers)
There is an injection .
Order
Definition
(Positive numbers)
Given and , a decimal fraction is positive if : i.e. the predicate is defined as
Proposition
(Decidability of positive numbers)
Given , , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every integer , is decidable for every integer and natural number .
Definition
(Less than)
For every decimal fraction and , there is a proposition called less than and defined as
Proposition
(Decidability of less than)
Given and , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every decimal fraction , and is decidable for every decimal fraction and .
Definition
(Negative numbers)
Given and , a decimal fraction is negative if ; i.e. the predicate is defined as
Proposition
(Decidability of negative numbers)
Given , , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every integer , is decidable for every integer and natural number
Definition
(Greater than)
For every decimal fraction and , there is a proposition called greater than and defined as
Proposition
(Decidability of greater than)
Given and , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every decimal fraction , and is decidable for every decimal fraction and .
Definition
(Non-negative numbers)
Given and , a decimal fraction is non-negative if ; i.e. the predicate is defined as
Proposition
(Decidability of non-negative numbers)
Given , , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every integer , is decidable for every integer and natural number
Definition
(Less than or equal to)
For every decimal fraction and , there is a proposition called less than or equal to and defined as
Proposition
(Decidability of less than or equal to)
Given and , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every decimal fraction , and is decidable for every decimal fraction and .
Definition
(Non-positive numbers)
Given and , a decimal fraction is non-positive if ; i.e. the predicate is defined as
Proposition
(Decidability of non-positive numbers)
Given , , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every integer , is decidable for every integer and natural number
Definition
(Greater than or equal to)
For every decimal fraction and , there is a proposition called greater than or equal to and defined as
Proposition
(Decidability of greater than or equal to)
Given and , the predicate is a decidable proposition.
Proof
By definition, is the same as . Because the relation is decidable for every decimal fraction , and is decidable for every decimal fraction and .
Definition
(Non-zero numbers)
Given and , a decimal fraction is non-zero if ; i.e. the predicate is defined as
Proposition
(ordered integral domain)
The decimal fractions form an ordered integral domain.
Definition
(Ramp)
There exists a function called ramp and defined as
for , .
Definition
(Minimum)
There exists a binary operation called minimum defined as
for , .
Definition
(Maximum)
There exists a binary operation called maximum defined as
for , .
Definition
(Absolute value)
There exists a function called absolute value and defined as
for .
Proposition
(total order)
The decimal fractions are a totally ordered ring.
Scientific notation
Proposition
(scientific notation)
For all decimal fractions , if , then there exists an integer such that and .
Algebraic closure
The algebraic closure of the rational numbers is called the field of algebraic numbers, and is thus isomorphic to \overline{\mathbb{Q}}, the algebraic closure of the rational numbers.
Topologies
There are several interesting topologies on that make into a topological group under addition, allowing us to define interesting fields by taking the completion with respect to this topology:
-
The discrete topology is the most obvious, which is already complete.
-
The absolute-value topology is defined by the metric ; the completion is the field of real numbers.
(This topology is totally disconnected.)
-
For prime numbers and , the -adic topology and -adic topology are defined by the ultrametric where is the highest exponent on and respectively in the prime factorization of ; the completions of each metric are the fields of -adic numbers and -adic numbers respectively.
Approximate division
Let be a Euclidean division function on the integers. Then there is a function called approximate division
to a sequence of decimal fractions called the infinite decimal representation of the rational number
This sequence in general does not converge in the decimal rational numbers; the initial archimedean integral domain in which every infinite decimal representation of a rational number converges is the rational numbers.
References