TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

$C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$

Statement

$C = R [x] / (x^{2} + 1)$ is a field containing the embedded copy of $R$ . Every complex number has a unique form $a + b i$ with $a, b \in R$ , and $(a + b i) + (u + v i) = (a + u) + (b + v) i,$ $(a + b i) (u + v i) = (a u - b v) + (a v + b u) i .$ If $a + b i \neq 0$ , then $(a + b i)^{- 1} = \frac{a - b i}{a^{2} + b^{2}} .$

Facts & Assumptions

Given: The quotient construction $C = R [x] / (x^{2} + 1)$ .

[F1]

The polynomial $x^{2} + 1$ is irreducible over $R$ ( $x^{2} + 1$ is irreducible over $R$ ).

[F2]

For a monic irreducible polynomial $p$ of degree $n$ , $F [x] / (p)$ is a field extension of $F$ and every class has a unique representative of degree below $n$ ( $F [x] / (p)$ for monic irreducible $p$ is a field extension containing the root $x + (p)$ with unique reduced representatives).

[F3]

The real numbers form an ordered field (The reals form a totally ordered field).

[F4]

In an ordered field every nonzero square is positive (Squares of nonzero elements are positive).

[F5]

$C$ is the quotient $R [x] / (x^{2} + 1)$ and $i = x + (x^{2} + 1)$ (The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ).

Proof

technique · direct

1.1F1F2F5

Apply [F2] to [F1]. With the construction in [F5], this proves that $C$ is a field, that the constant-class map embeds $R$ , and that every class has a unique representative $a + b x$ , hence a unique form $a + b i$ .

2.1F5step 1.1algebra

Quotient addition and multiplication, followed by $i^{2} = - 1$ , give the two displayed coordinate formulas. All field axioms are inherited from the field in step 1.1.

2.2F3F4step 1.1

If $a + b i \neq 0$ , uniqueness in step 1.1 gives $a \neq 0$ or $b \neq 0$ . The corresponding square is positive by [F4], the other square is nonnegative, and therefore $a^{2} + b^{2} > 0$ in the ordered field [F3].

3.1step 2.1step 2.2algebra∎

Direct multiplication using step 2.1 gives $(a + b i) (a - b i) = a^{2} + b^{2}$ . Since the real denominator is nonzero by step 2.2, division proves the inverse formula.

Depends on

Dependency tree · 2 levels

Sources

T. Judson, Abstract Algebra: Theory and Applications, Extension Fields