Definition·D056
The integers
Equivalence classes of pairs of naturals under equal cross-sums: each class is a difference.
In words
Two pairs of natural numbers are declared equivalent when their cross sums agree. The integers are the classes of pairs of natural numbers under this equivalence relation: each class represents a difference.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Read
as "
minus
":
is
,
is
, and
is
, each a class of infinitely many representative pairs (e.g.
). By L41,
really is an equivalence relation, which is what makes this quotient meaningful. The natural numbers embed into
via D057; addition and multiplication are defined representative-wise in D058 and D060. This is a special case of the general "Grothendieck group completion" construction, which turns any commutative monoid (here
) into a group.