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 irreducible over
Statement
The polynomial is irreducible in .
Facts & Assumptions
Given: The polynomial .
The real numbers form an ordered field (The reals form a totally ordered field).
In an ordered field, the square of every nonzero element is positive (Squares of nonzero elements are positive).
A polynomial of degree two or three over a field is irreducible if and only if it has no root in that field (A polynomial of degree two or three over a field is irreducible exactly when it has no root in the field).
Proof
For , either , so , or [F2] gives . Thus by the ordered-field laws in [F1].
Hence has no real root.
Since it has degree two, [F3] now gives its irreducibility over .
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
- Primary decomposition over ℚ with one linear and one irreducible quadratic factor Example
- Quarter-turn rotation is not diagonalisable over ℝ but is diagonalisable over ℂ Example
- x²+1 is irreducible over ℝ and split over ℂ Example
- FALSE: every irreducible polynomial in ℝ[x] has degree 1 False statement
- FALSE: every polynomial with real coefficients has a real root False statement
- FALSE: the real numbers are algebraically closed False statement
- ℂ=ℝ[x]/(x²+1) is a field, every element is uniquely a+bi, and every nonzero element has inverse (a-bi)/(a²+b²) Theorem
Dependency tree · two levels
15 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)