Definition·D069
Multiplicative inverse of a rational
The multiplicative inverse of a nonzero rational, obtained by swapping the coordinates of a representative pair.
For
with
(so
), define
the multiplicative inverse of
.
In words
With x nonzero (so a nonzero), the inverse x⁻¹ is the swapped pair (b,a).
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
That
: the class equals
(
from D064)
exactly when
, i.e.
, using the unity law of T23 and zero times anything is zero. Well-definedness (independence from the choice of representative, and that
is itself representative-independent) is L59. That
is verified in T27.