CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-29

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.

Realification doubles finite dimension

Statement

If $W$ is a finite-dimensional complex vector space with $\dim_{C} W = n$ , then its realification $W_{R}$ of Realification of a complex vector space by restriction of scalars is finite-dimensional over $R$ with

$\dim_{R} W_{R} = 2 n .$

Facts & Assumptions

Given: A finite-dimensional complex vector space $W$ with $\dim_{C} W = n$ .

[L1]

The realification $W_{R}$ is the real vector space with the same underlying set and addition, and scalar multiplication restricted to $R \subseteq C$ (Realification of a complex vector space by restriction of scalars).

[L2]

In $C = R [x] / (x^{2} + 1)$ with $i = x + (x^{2} + 1)$ , every complex number is written uniquely as $a + b i$ with $a, b \in R$ and $i^{2} = - 1$ (The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ ).

[L3]

A basis is a linearly independent spanning set (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

[L4]

The dimension of a finite-dimensional vector space is the size of any of its bases (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

Proof

technique · direct

1.1

Choose an ordered complex basis $(e_{1}, \dots, e_{n})$ of $W$ , which exists because $W$ is finite-dimensional over $C$ by [L4].

L4choose

2.1

The list $(e_{1}, i e_{1}, \dots, e_{n}, i e_{n})$ spans $W_{R}$ : writing $w = \sum_{j} z_{j} e_{j}$ and $z_{j} = a_{j} + i b_{j}$ by [L2], one has $w = \sum_{j} a_{j} e_{j} + \sum_{j} b_{j} (i e_{j})$ by the scalar-multiplication restriction of [L1].

step 1.1L1L2algebra

2.2

The list is linearly independent over $R$ : if $\sum_{j} a_{j} e_{j} + \sum_{j} b_{j} (i e_{j}) = 0$ with real coefficients, then $\sum_{j} (a_{j} + i b_{j}) e_{j} = 0$ in $W$ , so the complex independence of $(e_{1}, \dots, e_{n})$ forces every $a_{j} + i b_{j} = 0$ and hence every $a_{j} = b_{j} = 0$ ; in particular the displayed entries are pairwise distinct.

step 1.1L3algebra

3.1

By [L3], steps 2.1 and 2.2 make the displayed list a real basis of $W_{R}$ with $2 n$ entries, so [L4] gives $\dim_{R} W_{R} = 2 n$ .

step 2.1step 2.2L3L4∎

Depends on

Used by

Realifying ℂⁿ gives ℝ²ⁿ with basis e₁,ie₁,…,eₙ,ieₙ Example

Dependency tree · two levels

24 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

Keith Conrad, Complexification (notes) (standard reference, not scraped)
Mikhail Troshkin, Real-complex linear algebra and abelian varieties (standard reference, not scraped)