Alphabeta MathSimple Field Extensions and the Construction of the Complex Numbers
About this page
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.
✓ 17 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 17 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
- Binary Operations, Monoids, Groups and Subgroups
- Cosets, Index and Lagrange's Theorem
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Normal Subgroups and Quotient Groups
- Polynomial Rings, the Division Algorithm and Roots
- Rings, Subrings, Integral Domains and Fields
Real Analysis
2 · Logical flowchart
3 · Items
Definition
Field extensions, generated subrings F[S], generated subfields F(S), and simple extensions
Corollary
The composite of two subfields is the subfield generated by their union
Definition
Algebraic and transcendental elements and algebraic extensions
Theorem
The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element
Theorem
A simple transcendental extension consists exactly of rational expressions in its generator
Theorem
Two simple transcendental extensions are uniquely F-isomorphic once their generators are matched
Theorem
F[x]/(p) for monic irreducible p is a field extension containing the root x+(p) with unique reduced representatives
Corollary
Every nonconstant polynomial over a field has a root in some field extension
Theorem
Universal property of adjoining a root of an irreducible polynomial
Theorem
A simple algebraic extension is its minimal-polynomial quotient and has power basis 1,a,…,aⁿ⁻¹ and degree n
Corollary
Stem fields of a monic irreducible polynomial are uniquely F-isomorphic when their distinguished roots are matched
Lemma
x²+1 is irreducible over ℝ
Definition
The complex numbers as ℝ[x]/(x²+1), with the real embedding and imaginary unit i
Theorem
ℂ=ℝ[x]/(x²+1) is a field, every element is uniquely a+bi, and every nonzero element has inverse (a-bi)/(a²+b²)
Theorem
ℂ is the real coordinate plane, with coordinate arithmetic
Corollary
ℂ/ℝ has power basis 1,i and degree 2
Corollary
A square root of -1 in a real field extension determines a unique real-field homomorphism from ℂ
Definition
Real and imaginary parts, complex conjugation, and modulus
Lemma
Conjugation is an involutive real-field automorphism, zz̄=|z|², and modulus is definite, multiplicative, and subadditive
Theorem
The only real-field automorphisms of ℂ are the identity and complex conjugation
Theorem