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.
The reals form a field
Statement
(The real numbers) is a field.
Facts & Assumptions
Given: Classes .
is an ideal of (Null sequences form an ideal).
is a commutative ring with (Cauchy sequences form a commutative ring).
Maximality construction: for non-null there is Cauchy with null (The null ideal is maximal).
The constant sequence is not a null sequence (its terms stay at ), so is a proper ideal and (Null sequence).
Proof
Operations on classes via representatives are well defined: for , and , since ideals absorb products and sums.
The ring axioms descend to the quotient because the operations are well defined and is a ring, verified on representatives; since the constant sequence is not null.
Inverses: a nonzero class has a non-null representative ; taking from the maximality construction, , so is a multiplicative inverse of .
is a commutative ring with in which every nonzero element is invertible: a field.
Depends on
Used by
- For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries Corollary
- The first quadrant of ℝ² contains 0 and is closed under addition and is not a linear subspace, since it is not closed under multiplication by -1 Counterexample
- For n≥1, the determinant over a commutative ring by the Leibniz formula, and |det A| for a real matrix Definition
- The quaternions ℍ: real quadruples with componentwise addition and an explicit multiplication formula matching the table on 1, i, j, k Definition
- A consistent underdetermined system has an affine two-parameter solution set Example
- For any field F, (F, +) and (F ∖ {0}, ·) are abelian groups; in particular (ℚ, +), (ℚ ∖ {0}, ·), (ℝ, +) and (ℝ ∖ {0}, ·) Example
- ℚ and ℝ are fields, hence commutative rings, integral domains and ordered rings, all of characteristic 0 Example
- ℝ as a vector space over ℚ has a basis, and every such basis is infinite; the existence proof exhibits none Example
- ℝ is a vector space over itself, over the embedded copy of ℚ by restriction of scalars, and over ℚ itself via the embedding Example
- The quarter-turn (x,y)↦(-y,x) on ℝ² has matrix beginpmatrix0&-11&0 endpmatrix and square -I₂ Example
- The rank and solution behaviour of a parameterised matrix change at one exceptional parameter Example
- The reals are the quotient of rational Cauchy sequences by the maximal ideal of null sequences Example
- The vector (1,2) ∈ ℝ² has coordinate list (1,2) in the standard ordered basis, (2,1) in its reversal, and (2,-1) in the ordered basis ((1,1),(1,0)) Example
- FALSE: det(A+B)=det(A)+det(B) for all same-sized square matrices False statement
- The rationals embed densely in the reals Lemma
- A finite square real matrix is invertible if and only if its determinant is nonzero Theorem
- Every invertible finite square real matrix is a finite product of elementary matrices Theorem
- ℍ is a division ring that is not commutative, hence not a field: q⁻¹ = bar q / N(q) for q ≠ 0, while ij = k and ji = -k Theorem
- The reals form a totally ordered field Theorem
Cited to discharge well-definedness by The real numbers.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 20 results over 14 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
- T. Tao, Analysis I, 3rd ed., §5.3 (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
- L. S. Krapp, Constructions of the real numbers: a set theoretical approach (Oxford, 2014) (standard reference, not scraped)