LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-28

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 real Jacobian determinant of a complex-linear automorphism is the squared modulus of its complex determinant

Statement

Let $m \geq 1$ , let $L : C^{m} \to C^{m}$ be $C$ -linear, and let $A$ be its matrix in the standard complex basis. Regard $L$ as an $R$ -linear map on $R^{2 m}$ through the usual identification $C^{m} ≅ R^{2 m}$ . Then

$\det_{R} L = {∣ \det_{C} A ∣}^{2} .$

In particular $\det_{R} L \neq 0$ if and only if $\det_{C} A \neq 0$ .

Facts & Assumptions

Given: The complex-linear map $L$ and its matrix $A = B + i C$ with real matrices $B$ and $C$ .

[L1]

Determinants multiply under matrix products, and the determinant of a triangular block matrix is the product of its diagonal-block determinants (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , The determinant of a triangular matrix is the product of its diagonal entries).

[A1]

In the real basis $(e_{1}, \dots, e_{m}, i e_{1}, \dots, i e_{m})$ , the real matrix of $L$ is

$R = (\begin{array}{cc} B & - C \\ C & B \end{array}) .$

The complex matrices

$P = \frac{1}{2} (\begin{array}{cc} I & I \\ - i I & i I \end{array}), Q = (\begin{array}{cc} I & i I \\ I & - i I \end{array})$

are inverse to one another.

Proof

technique · direct

1.1

Using [A1], direct block multiplication gives $Q R P = (\begin{array}{cc} A & 0 \\ 0 & \overline{A} \end{array}) .$ Indeed the two columns of $P$ are the $(z, \overline{z})$ coordinates of a real vector, and the $C$ -linearity of $L$ makes the transformed action split into $A$ on the $z$ block and $\overline{A}$ on the $\overline{z}$ block.

A1algebra

2.1

By [L1], step 1.1, and the identity $Q P = I$ , one has $\det_{C} R = \det_{C} (Q R P) = \det_{C} A \cdot \det_{C} \overline{A} = \det_{C} A \cdot \overline{\det_{C} A} = {∣ \det_{C} A ∣}^{2} .$ Since $R$ has real entries, the determinant polynomial gives the same real number whether computed over $R$ or over $C$ , so $\det_{R} L = \det_{C} R$ .

step 1.1L1algebra

3.1

The displayed formula immediately makes $\det_{R} L$ nonzero exactly when $\det_{C} A$ is nonzero.

step 2.1∎

Depends on

Used by

The holomorphic inverse function theorem in several complex variables Theorem

Dependency tree · two levels

23 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

Jiří Lebl, Tasty Bits of Several Complex Variables, Section 5.2 (standard reference, not scraped)
Jaap Korevaar and Jan Wiegerinck, Several Complex Variables, Section 5.2 (standard reference, not scraped)