Definition·D066
Negation of a rational
The additive inverse of a rational, obtained by negating the numerator of a representative pair.
For
, define
(with
the negation of the integer
), the additive inverse of
.
In words
The negation of a rational is obtained by negating the numerator 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.
, applying substitutivity (negating both sides) and the sign rule for negating a product gives
, which says exactly
. So
does not depend on the choice of representative for
. Combined with T26, this makes
the unique additive inverse (L28).