Definition·D059
Negation of an integer
The additive inverse of an integer, obtained by swapping the coordinates of a representative pair.
For
, define
the additive inverse of
:
.
In words
The negation of an integer is obtained by swapping the two coordinates of any representative pair; it is the additive inverse.
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
Well defined: if
, i.e.
, then commuting both sides (commutativity) gives
, and reading this equation from right to left (symmetry) gives
, which says exactly
, so
does not depend on the choice of representative for
. T22 already identifies this class as an additive inverse of
, and L28 makes it the inverse, since inverses in a group are unique.