TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

For the linear-first convention, a basis change by $P$ sends a sesquilinear matrix $A$ to $P^{T} A σ (P)$ ; Hermitian forms satisfy $A = σ (A)^{T}$

Statement

Let $H$ be sesquilinear over a field with involution $σ$ , using the convention linear in the first variable. If its old matrix is $A$ and a basis change has matrix $P$ , then its new matrix is

$P^{T} A σ (P),$

where $σ (P)$ is obtained entrywise. Moreover, $H$ is Hermitian if and only if $A = σ (A)^{T}$ .

Facts & Assumptions

Given: A field involution $σ$ , a sesquilinear form $H$ , and the displayed basis data.

[L1]

Sesquilinearity is linear in the first variable and $σ$ -linear in the second; Hermitian symmetry is $H (u, v) = σ (H (v, u))$ (Sesquilinear and Hermitian forms over a field with an involution, using the convention linear in the first variable).

[L2]

Matrix multiplication expands as the corresponding finite row-column sums (Matrix multiplication is associative, unital, distributive, and compatible with scalar multiplication).

[L3]

Transpose reverses products (Transpose is linear and involutive, and $(A B)^{T} = B^{T} A^{T}$ ).

Proof

technique · coordinate calculation

1.1

If $x, y$ are new coordinate columns, their old columns are $P x, P y$ . Expanding [L1] in an old basis gives $H (u, v) = (P x)^{T} A σ (P y) = x^{T} P^{T} A σ (P) σ (y)$ .

L1L2L3algebra

1.2

In a basis $(e_{i})$ , Hermitian symmetry is $A_{i j} = H (e_{i}, e_{j}) = σ (H (e_{j}, e_{i})) = σ (A_{j i})$ for every $i, j$ , which is exactly $A = σ (A)^{T}$ .

L1algebra

2.1

Since step 1.1 holds for every $x, y$ , the new matrix is $P^{T} A σ (P)$ . This includes the identity involution, where it reduces to ordinary congruence.

step 1.1

2.2

Conversely, if $A = σ (A)^{T}$ , the coordinate formula and $σ^{2} = id$ give $H (u, v) = σ (H (v, u))$ for arbitrary coordinate columns, so $H$ is Hermitian.

step 1.2L1L2L3algebra

3.1

Steps 2.1, 1.2, and 2.2 prove the basis-change formula and both directions of the Hermitian criterion.

step 2.1step 1.2step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 23 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

H. Pinkham, Linear Algebra, §7.8 (standard reference, not scraped)

For the linear-first convention, a basis change by PP sends a sesquilinear matrix AA to PTA σ(P)PTAσ(P); Hermitian forms satisfy A=σ(A)TA=σ(A)T