ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$Frac (Z)$ is canonically isomorphic to $Q$

Example

The field of fractions of $Z$ is canonically isomorphic to $Q$ by $\frac{a}{b} ⟼ \frac{a}{b}, a, b \in Z, b \neq 0.$

Facts & Assumptions

Given: The standard inclusion $Z ↪ Q$ .

[F1]

The rationals are the equivalence classes written $a / b$ for integers $a, b$ with $b \neq 0$ (The rationals as equivalence classes of pairs of integers).

[F2]

The rationals form a field (The rationals form a field).

[F3]

An injective ring map from a domain into a field extends uniquely to its field of fractions (Every injective ring map from a domain into a field factors uniquely through its field of fractions).

[F4]

The integers form a commutative ring (The integers form a commutative ring).

[F5]

A product of two nonzero integers is nonzero (The integers have no zero divisors; multiplicative cancellation).

[F6]

The natural numbers embed injectively in the integers, while $0$ and $1$ are distinct natural numbers (The naturals embed in the integers, The natural numbers $N$ (von Neumann)).

[F7]

An integral domain is a commutative ring with $1 \neq 0$ and no zero divisors (Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors).

Verification

technique · direct

1.1

Facts [F4] and [F5] give the commutative-ring and no-zero-divisor clauses for $Z$ , while [F6] gives $1 \neq 0$ ; hence [F7] makes $Z$ an integral domain. The map $a \mapsto a / 1$ from $Z$ to $Q$ is injective by the defining equivalence relation in [F1]. Since $Q$ is a field by [F2], [F3] extends it uniquely to an injective homomorphism $Frac (Z) \to Q$ with the displayed formula.

F1F2F3F4F5F6F7

2.1

Every rational is $a / b$ with $b \neq 0$ by [F1], so the homomorphism is surjective and hence an isomorphism. It fixes each integer, which makes it canonical over $Z$ .

F1step 1.1∎

Depends on

Used by

Dependency tree · two levels

39 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

The CRing Project, Chapter 13: Fields and Extensions (standard reference, not scraped)

Frac⁡(Z)Frac(Z) is canonically isomorphic to QQ