ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

${1 + i, 1 - i}$ is a normal basis of $C / R$ while ${1, i}$ is not

Example

The extension $C / R$ (The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ) is finite Galois of degree two with $Gal (C / R) = {i d, z \mapsto \overline{z}}$ (Real and imaginary parts, complex conjugation, and modulus). For it:

the conjugate list $(1 + i, 1 - i)$ is a normal basis (Normal bases of a finite Galois extension);
$(1, i)$ is an $R$ -basis of $C$ that is not a conjugate list of any element;
$(i, - i)$ is the conjugate list of $i$ but is not a basis.

The last two show that the two conditions in the definition of a normal basis are independent of each other.

Facts & Assumptions

Given: The complex field with $i^{2} = - 1$ and conjugation $\overline{a + b i} = a - b i$ for $a, b \in R$ (Real and imaginary parts, complex conjugation, and modulus); in $R$ one has $2 \neq 0$ .

[L1]

$C = R (i)$ is a simple algebraic extension with power basis $1, i$ and $[C : R] = 2$ ( $C / R$ has power basis $1, i$ and degree $2$ , The degree $[K : F] = \dim_{F} K$ of a finite field extension).

[L2]

Every field automorphism of $C$ fixing $R$ pointwise is either the identity or complex conjugation, and these two are distinct (The only real-field automorphisms of $C$ are the identity and complex conjugation, Relative field automorphisms and $Aut (K / F)$ ).

[L3]

Complex conjugation is a real-field automorphism (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L4]

A finite extension $K / F$ with $G = Aut (K / F)$ is Galois exactly when $∣ G ∣ = [K : F]$ (Equivalent characterizations of a finite Galois extension, Finite Galois extensions and $Gal (K / F)$ ).

[L5]

A list $v$ of length $n$ is an ordered basis of $V$ if and only if every $x \in V$ has exactly one coordinate list with respect to it (A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis); and $\dim V = \dim \ker T + \dim im T$ for a linear $T$ on a finite-dimensional $V$ (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[L6]

Every finite Galois extension of an infinite field has a normal basis (Every finite Galois extension of an infinite field has a normal basis).

Verification

technique · direct

1.1

By [L2] and [L3] the group $Aut (C / R)$ has exactly the two elements $i d$ and conjugation, so its order is $2 = [C : R]$ by [L1]; hence $C / R$ is finite Galois with that Galois group by [L4].

L1L2L3L4

2.1

The conjugate list of $1 + i$ is $(1 + i, 1 - i)$ , whose members have coordinate lists $(1, 1)$ and $(1, - 1)$ in the ordered basis $(1, i)$ of [L1]. For $a, b \in R$ , $a (1 + i) + b (1 - i) = (a + b) + (a - b) i$ vanishes exactly when $a + b = 0$ and $a - b = 0$ , hence when $2 a = 0$ , that is $a = 0$ and then $b = 0$ .

step 1.1L1given

2.2

$(1, i)$ is a basis by [L1], but no $z \in C$ has conjugate list $(z, \overline{z})$ with underlying set ${1, i}$ : such a $z$ would lie in ${1, i}$ , and the set for $z = 1$ is ${1}$ while for $z = i$ it is ${i, - i}$ , neither of which is ${1, i}$ .

step 1.1L1given

3.1

So the linear map $R^{2} \to C$ sending $(a, b)$ to $a (1 + i) + b (1 - i)$ has trivial kernel; both spaces have dimension two by [L1], so [L5] makes it bijective and $(1 + i, 1 - i)$ an ordered $R$ -basis of $C$ . Being the conjugate list of $1 + i$ , it is a normal basis, in agreement with [L6].

step 1.1step 2.1L1L5L6

4.1

$(i, - i)$ is the conjugate list of $i$ , since $\overline{i} = - i$ , and its two members are distinct; but $1 \cdot i + 1 \cdot (- i) = 0$ is a vanishing combination with nonzero coefficients, so the list is not independent and by [L5] is not a basis. With steps 3.1 and 2.2 this establishes all three claims.

step 1.1step 3.1step 2.2L5given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

68 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

K. Conrad, Linear Independence of Characters (expository blurb), Examples 3.1-3.3 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, the normal basis theorem (standard reference, not scraped)

{1+i, 1−i}{1+i,1−i} is a normal basis of C/RC/R while {1,i}{1,i} is not