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 complex numbers as , with the real embedding and imaginary unit
Definition
Form the polynomial ring (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution) and define the complex numbers by the quotient ring (The quotient ring with ). Write for the constant class and set Thus in the quotient. The constant-class map is the specified real map; its injectivity and the field structure are proved in is a field, every element is uniquely , and every nonzero element has inverse ↗, after which is a field extension in the sense of Field extensions, generated subrings , generated subfields , and simple extensions.
Depends on
Used by
- A square root of -1 in a real field extension determines a unique real-field homomorphism from ℂ Corollary
- ℂ/ℝ has power basis 1,i and degree 2 Corollary
- Realification doubles finite dimension Corollary
- Complexification as ℂ⊗_ℝV with its canonical real-linear embedding Definition
- Realification of a complex vector space by restriction of scalars Definition
- Self-adjoint complex function algebras, unitality, and point separation Definition
- The complex exponential by its power series Definition
- {1+i, 1-i} is a normal basis of ℂ/ℝ while {1,i} is not Example
- ℂ⊗_ℝℂ≅ℂ×ℂ as ℝ-algebras Example
- Quarter-turn rotation is not diagonalisable over ℝ but is diagonalisable over ℂ Example
- The real 2-dimensional irreducible representation of C₃ has endomorphism ring ℂ Example
- FALSE: the complex field admits an order making it an ordered field False statement
- Canonical Banach complexification of a real Banach space Lemma
- The Cauchy product of two absolutely convergent complex series converges absolutely to the product of their sums Lemma
- ℂ=ℝ[x]/(x²+1) as the Euclidean plane and as a normed real algebra: what the identification preserves Remark
- ℂ=ℝ[x]/(x²+1) is a field, every element is uniquely a+bi, and every nonzero element has inverse (a-bi)/(a²+b²) Theorem
- The only real-field automorphisms of ℂ are the identity and complex conjugation Theorem
Dependency tree · two levels
13 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
- T. Judson, Abstract Algebra: Theory and Applications, Extension Fields (standard reference, not scraped)