Skip to content
Axiomatic Wiki

WLThe embedding of the integers is injective

Lemma·L56

Distinct integers give distinct rationals.

(D064) is injective: for , if then .
In words
If two integers give the same rational under the embedding, they were already the same integer.
Rests onF02F03F04F05F06F08F09F11F12F13F14A01A02A06A08
Never needed: F10 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Suppose , i.e. . By T04 applied to ≃, this holds exactly when , i.e. .
  2. 2
    By the unity law of T23, and , so .
∎

Remarks

Compatibility of with and is immediate from D065/D067 the same way L46 was for , though not separately stated as its own article; together with injectivity, is a faithful copy of sitting inside .
Wikipedia ↗Rat.ofInt_inj ↗

Used by

T27
Propose an edit1 published revision