CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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$ has power basis $1, i$ and degree $2$

Statement

The complex field is a simple algebraic extension $C = R (i)$ . Its power basis is $1, i$ , and $[C : R] = 2$ .

Facts & Assumptions

Given: The real field extension $C / R$ generated by $i$ .

[F1]

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

[F2]

For $a$ algebraic over $F$ with minimal polynomial $m_{a}$ of degree $n$ , every element of $F (a)$ is uniquely $c_{0} + c_{1} a + \dots + c_{n - 1} a^{n - 1}$ , so $1, a, \dots, a^{n - 1}$ is the power basis and $[F (a) : F] = n$ (A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ ).

[F3]

Every complex number is uniquely $a + b i$ ( $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})$ ), and $i^{2} = - 1$ (The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ).

[F4]

A root of a nonzero polynomial is algebraic (Algebraic and transcendental elements and algebraic extensions); for an algebraic element with minimal polynomial $m_{a}$ , $f (a) = 0$ exactly when $m_{a}$ divides $f$ (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

Proof

technique · direct

1.1

By [F3], $i$ is a root of $x^{2} + 1$ , and [F1] and [F4] make that polynomial its minimal polynomial.

F1F3F4

1.2

The unique coordinate form in [F3] gives $C = R (i)$ .

2.1

Apply [F2] to step 1.1: the power basis is $1, i$ and the degree is $2$ .

F2step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 58 results over 10 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. Judson, Abstract Algebra: Theory and Applications, Extension Fields (standard reference, not scraped)

C/RC/R has power basis 1,i1,i and degree 22