DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 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.

Complexification of a real-linear map

Definition

Let $T : V \to W$ be a real-linear map between real vector spaces (Linear map between vector spaces over the same field). Its complexification is the $R$ -linear map

$T_{C} : = {id}_{C} \otimes T : C \otimes_{R} V ⟶ C \otimes_{R} W, T_{C} (z \otimes v) : = z \otimes T (v) .$

Existence. The map $(z, v) \mapsto z \otimes T (v)$ from $C \times V$ to $C \otimes_{R} W$ is additive in each variable and $R$ -balanced because $T$ is real-linear, so Universal property of the tensor product for balanced maps into abelian groups supplies the unique $R$ -linear map with the displayed value on elementary tensors.

Remarks

The map $T_{C}$ is complex-linear on the complexifications of Complexification as $C \otimes_{R} V$ with its canonical real-linear embedding: for $z, z^{'} \in C$ and $v \in V$ ,

$T_{C} (z^{'} \cdot (z \otimes v)) = T_{C} ((z^{'} z) \otimes v) = (z^{'} z) \otimes T (v) = z^{'} \cdot (z \otimes T (v)) = z^{'} \cdot T_{C} (z \otimes v),$

so the identities extend from elementary tensors to all of $C \otimes_{R} V$ by additivity.

Depends on

Used by

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)