TheoremStatement: AI-adaptedProof: 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.

The determinant of a linear operator is independent of the chosen ordered basis

Statement

Let $T : V \to V$ be a linear operator on a finite-dimensional vector space over a field. If $\dim V \geq 1$ and $B$ and $C$ are ordered bases of $V$ , then

$\det ([T]_{B}) = \det ([T]_{C}) .$

In dimension zero the operator determinant is the separately defined value $1$ . Consequently The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space is well defined in every finite dimension.

Facts & Assumptions

Given: $T, V, B, C$ as in the statement.

[F1]

The proposed value of $\det (T)$ in positive dimension is the determinant of a representing matrix, while in dimension zero it is $1$ (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space).

[L1]

In positive dimension the representing-matrix determinant is the unique scalar by which $T$ scales every alternating top-degree form (On a positive-dimensional space, $\det (T)$ is the unique scalar by which $T$ scales every alternating top-degree form).

Proof

technique · direct

1.1

If $\dim V = 0$ , [F1] defines the operator determinant directly as $1$ ; no determinant of a $0 \times 0$ representing matrix is invoked.

1.2

Suppose $\dim V \geq 1$ . Applying [L1] first with $B$ and then with $C$ characterises both $\det ([T]_{B})$ and $\det ([T]_{C})$ as the same unique basis-free scaling scalar.

2.1

The two matrix determinants are therefore equal in positive dimension; together with the separate zero-dimensional definition in step 1.1, this proves well-definedness in every finite dimension.

step 1.1step 1.2∎

Depends on

Used by

Cited to discharge well-definedness by The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and 1 on the zero space.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 9 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

Sheldon Axler, Linear Algebra Done Right, 4th ed. (standard reference, not scraped)