ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

The standard embedding $R^{n} ↪ C^{n}$ is the canonical complexification map

Example

Take $V = R^{n}$ with its standard real basis $e_{1}, \dots, e_{n}$ . The identification

$C \otimes_{R} R^{n} ≅ C^{n}, z \otimes e_{j} ⟼ z e_{j},$

carries the canonical embedding $ι x = 1 \otimes x$ of Complexification as $C \otimes_{R} V$ with its canonical real-linear embedding to the standard inclusion $R^{n} ↪ C^{n}$ that views a real coordinate vector as a complex one. For $n = 0$ both sides are the zero space.

Facts & Assumptions

Given: The standard real basis $(e_{1}, \dots, e_{n})$ of $R^{n}$ and the canonical embedding $ι$ .

[L1]

The complexification $V_{C} = C \otimes_{R} V$ carries the scalar action $z \cdot (w \otimes v) = (z w) \otimes v$ and the real-linear embedding $ι v = 1 \otimes v$ (Complexification as $C \otimes_{R} V$ with its canonical real-linear embedding).

[L2]

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

[L3]

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

Verification

technique · direct

1.1

The list $(e_{1}, \dots, e_{n})$ is a real basis of $R^{n}$ by definition of the standard basis.

given

1.2

By [L2], $C \otimes_{R} R^{n} ≅ R^{n} \oplus i R^{n}$ through $Φ$ , and the assignment $(x, y) \mapsto x + i y$ , taken coordinatewise, is a complex-linear isomorphism $R^{n} \oplus i R^{n} \to C^{n}$ : complex scalar multiplication $(a + b i) \cdot (x, y) = (a x - b y, a y + b x)$ is sent to $(a x - b y) + i (a y + b x) = (a + b i) (x + i y)$ .

L2algebra

2.1

Composing, the element $z \otimes e_{j}$ maps to $z (e_{j}, 0)$ and then to the $j$ th standard complex vector scaled by $z$ ; additivity extends this to every tensor.

step 1.2algebra

3.1

For $x = (x_{1}, \dots, x_{n})$ one has $ι x = 1 \otimes x = \sum_{j} x_{j} (1 \otimes e_{j})$ , which step 2.1 sends to $\sum_{j} x_{j} e_{j} = x$ ; this is exactly the standard inclusion of $R^{n}$ into $C^{n}$ , and by [L3] the images $ι e_{j} = e_{j}$ form the complex basis of the complexification.

L1L3step 2.1

4.1

Steps 1.2 and 3.1 identify the complexification with $C^{n}$ and the canonical embedding with the standard inclusion.

step 1.2step 3.1∎

Depends on

Used by

FALSE: complexification doubles finite dimension False statement

Dependency tree · two levels

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

The standard embedding Rn↪CnRn↪Cn is the canonical complexification map