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

Transpose is linear, sends identities to identities, and reverses composition: $(S \circ T)^{} = T^{} \circ S^{*}$

Statement

For linear maps $T, T^{'} : V \to W$ , scalars $a, b$ , and $S : W \to X$ ,

$(a T + b T^{'})^{*} = a T^{*} + b T^{' *}, ({id}_{V})^{*} = {id}_{V^{*}}, (S \circ T)^{*} = T^{*} \circ S^{*} .$

Facts & Assumptions

Given: The displayed compatible linear maps and scalars.

[L1]

The transpose is $T^{*} (g) = g \circ T$ (The transpose or algebraic adjoint $T^{*} : W^{*} \to V^{*}$ , $T^{*} (g) = g \circ T$ , of a linear map $T : V \to W$ ).

[L2]

Composition of linear maps is associative, and identity maps are its identities (Identity maps and composites of linear maps are linear).

Proof

technique · pointwise evaluation

1.1

For $g \in W^{*}$ and $v \in V$ , $((a T + b T^{'})^{*} g) (v) = g (a T (v) + b T^{'} (v)) = a (T^{*} g) (v) + b (T^{' *} g) (v)$ , proving linearity in the map.

L1algebra

1.2

For $f \in V^{*}$ and $v \in V$ , $(({id}_{V})^{*} f) (v) = f (v)$ , so $({id}_{V})^{*} = {id}_{V^{*}}$ .

L1L2

1.3

For $h \in X^{*}$ , [L1] and associativity give $(S \circ T)^{*} (h) = h \circ S \circ T = T^{*} (S^{*} (h))$ , hence $(S \circ T)^{*} = T^{*} \circ S^{*}$ .

L1L2

2.1

Equality at every functional and vector proves all three asserted identities.

step 1.1step 1.2step 1.3∎

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: 7 results over 6 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, Chapter 6 (standard reference, not scraped)

Transpose is linear, sends identities to identities, and reverses composition: (S∘T)∗=T∗∘S∗(S∘T)∗=T∗∘S∗