Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck 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∘T)∗=T∗∘S∗

Statement

For linear maps T,T′:V→W, scalars a,b, and S:W→X,

(aT+bT′)∗=aT∗+bT′∗,(id⁡V)∗=id⁡V∗,(S∘T)∗=T∗∘S∗.

Facts & Assumptions

Given: The displayed compatible linear maps and scalars.

[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∈W∗ and v∈V, ((aT+bT′)∗g)(v)=g(aT(v)+bT′(v))=a(T∗g)(v)+b(T′∗g)(v), proving linearity in the map.

L1algebra
1.2

For f∈V∗ and v∈V, ((id⁡V)∗f)(v)=f(v), so (id⁡V)∗=id⁡V∗.

L1L2
1.3

For h∈X∗, [L1] and associativity give (S∘T)∗(h)=h∘S∘T=T∗(S∗(h)), hence (S∘T)∗=T∗∘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 · two levels

4 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