Alphabeta MathHow 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.
is canonically isomorphic to
Example
The field of fractions of is canonically isomorphic to by
Facts & Assumptions
Given: The standard inclusion .
The rationals are the equivalence classes written for integers with (The rationals as equivalence classes of pairs of integers).
The rationals form a field (The rationals form a field).
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).
The integers form a commutative ring (The integers form a commutative ring).
A product of two nonzero integers is nonzero (The integers have no zero divisors; multiplicative cancellation).
The natural numbers embed injectively in the integers, while and are distinct natural numbers (The naturals embed in the integers, The natural numbers (von Neumann)).
An integral domain is a commutative ring with and no zero divisors (Zero divisor, and integral domain: a commutative ring with and no zero divisors).
Verification
Facts [F4] and [F5] give the commutative-ring and no-zero-divisor clauses for , while [F6] gives ; hence [F7] makes an integral domain. The map from to is injective by the defining equivalence relation in [F1]. Since is a field by [F2], [F3] extends it uniquely to an injective homomorphism with the displayed formula.
Every rational is with by [F1], so the homomorphism is surjective and hence an isomorphism. It fixes each integer, which makes it canonical over .
Depends on
- The field of fractions $\operatorname{Frac}(D)=(D\setminus\{0\})^{-1}D$ of an integral domain
- Every injective ring map from a domain into a field factors uniquely through its field of fractions
- The rationals as equivalence classes of pairs of integers
- The rationals form a field
- The integers form a commutative ring
- The integers have no zero divisors; multiplicative cancellation
- The naturals embed in the integers
- The natural numbers $\mathbb{N}$ (von Neumann)
- Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 69 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- The CRing Project, Chapter 13: Fields and Extensions (standard reference, not scraped)