TheoremStatement: 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.

A real basis becomes a complex basis after complexification, so $\dim_{C} (C \otimes_{R} V) = \dim_{R} V$

Statement

Let $V$ be a real vector space with ordered basis $B = (v_{1}, \dots, v_{n})$ . Then $(ι v_{1}, \dots, ι v_{n})$ is an ordered complex basis of the complexification $V_{C}$ of Complexification as $C \otimes_{R} V$ with its canonical real-linear embedding. In particular, if $V$ is finite-dimensional then

$\dim_{C} (C \otimes_{R} V) = \dim_{R} V .$

Facts & Assumptions

Given: A real vector space $V$ with ordered basis $(v_{1}, \dots, v_{n})$ .

[L1]

If $M$ and $N$ are free with bases $(e_{i})$ and $(f_{j})$ , then $M \otimes N$ is free with basis $(e_{i} \otimes f_{j})$ (The elementary tensors of two bases form the product basis of the tensor product).

[L2]

The power basis $1, i$ is an $R$ -basis of $C$ , and $C = R (i)$ ( $C / R$ has power basis $1, i$ and degree $2$ ).

[L3]

The canonical isomorphism $Φ : C \otimes_{R} V \to V \oplus i V$ sends $z \otimes v$ to $z (v, 0)$ , with inverse $Ψ (v + i w) = 1 \otimes v + i \otimes w$ (The tensor and direct-sum models of complexification are canonically complex-linearly isomorphic).

[L4]

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).

[L5]

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

By [L2], ${1, i}$ is an $R$ -basis of $C$ , and by hypothesis $(v_{1}, \dots, v_{n})$ is an $R$ -basis of $V$ ; hence [L1] makes ${1 \otimes v_{j}, i \otimes v_{j} : j \leq n}$ an $R$ -basis of $C \otimes_{R} V$ .

L1L2L4

1.2

Transporting through the inverse isomorphism $Ψ$ of [L3], which sends $1 \otimes v_{j}$ to $v_{j}$ and $i \otimes v_{j}$ to $i v_{j}$ , the set ${v_{j}, i v_{j} : j \leq n}$ is an $R$ -basis of $V \oplus i V$ .

L3algebra

2.1

The vectors $v_{1}, \dots, v_{n}$ span $V \oplus i V$ over $C$ : every element $v + i w$ is $\sum_{j} a_{j} v_{j} + i \sum_{j} b_{j} v_{j} = \sum_{j} (a_{j} + i b_{j}) v_{j}$ by the real basis expansion of step 1.2.

step 1.2L4algebra

2.2

The vectors $v_{1}, \dots, v_{n}$ are complex-linearly independent: if $\sum_{j} (a_{j} + i b_{j}) v_{j} = 0$ , then $(\sum_{j} a_{j} v_{j}, \sum_{j} b_{j} v_{j}) = (0, 0)$ , so the real independence in step 1.2 forces every $a_{j} = b_{j} = 0$ .

step 1.2algebra

3.1

Steps 2.1 and 2.2 make $(v_{1}, \dots, v_{n})$ an ordered complex basis of the direct-sum model, and applying $Φ$ of [L3] carries it to the ordered complex basis $(ι v_{1}, \dots, ι v_{n})$ of $V_{C}$ .

step 2.1step 2.2L3L4

4.1

Both bases have exactly $n$ elements, so by [L5] the complex dimension of $V_{C}$ equals the real dimension of $V$ .

step 3.1L5∎

Depends on

Used by

Dependency tree · two levels

35 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)

A real basis becomes a complex basis after complexification, so dim⁡C(C⊗RV)=dim⁡RVdimC​(C⊗R​V)=dimR​V