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

In positive dimension the determinant of an operator is computed from a representing matrix by row reduction, tracking swaps and row scalings

Statement

Let $T$ be an operator on a positive-dimensional finite-dimensional vector space over a field, let $B$ be an ordered basis, and row-reduce $A = [T]_{B}$ to an upper triangular matrix $U$ . Each row addition leaves the determinant of the current matrix unchanged, each row swap changes its sign, each row scaling by $c \neq 0$ multiplies it by $c$ , and $\det (U)$ is the product of the diagonal entries of $U$ . Consequently, if the reduction uses $s$ swaps and scalings $c_{1}, \dots, c_{m}$ , then

$\det (T) = (- 1)^{s} (\prod_{j = 1}^{m} c_{j})^{- 1} \det (U) .$

Facts & Assumptions

Given: $T$ , an ordered basis $B$ , and $A = [T]_{B}$ .

[L1]

The operator determinant equals the determinant of its representing matrix in every ordered basis (The determinant of a linear operator is independent of the chosen ordered basis).

[L2]

Gaussian elimination over a field reduces every finite matrix to row echelon form (Gaussian elimination reduces every finite matrix over a field to row echelon form).

[L3]

A row swap negates a determinant, scaling one row by $c$ scales it by $c$ , and adding a scalar multiple of one row to another leaves it unchanged (For every square matrix, including singular ones, a row swap negates the determinant, scaling a row by any scalar scales it, and row addition leaves it unchanged).

[L4]

The determinant of a triangular square matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).

Proof

technique · direct

1.1

By [L1], $\det (T) = \det (A)$ , independently of the chosen basis.

1.2

Apply Gaussian elimination to $A$ and record, in order, every row operation used to reach an echelon matrix $U$ .

2.1

Reversing the recorded effects in [L3] expresses $\det (A)$ in terms of $\det (U)$ : each swap contributes a factor $- 1$ , each forward row scaling by $c \neq 0$ contributes a reverse factor $c^{- 1}$ , and a row addition contributes no factor.

step 1.2L3algebra

3.1

Since the square echelon matrix $U$ is upper triangular, [L4] gives $\det (U)$ as its diagonal product. With $s$ swaps and scalings $c_{1}, \dots, c_{m}$ , step 2.1 gives $\det (U) = (- 1)^{s} (\prod_{j} c_{j}) \det (A)$ , and step 1.1 identifies $\det (A)$ with $\det (T)$ ; solving for $\det (T)$ gives the displayed formula.

step 1.1step 2.1L4algebra∎

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: 38 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

Interactive Linear Algebra (standard reference, not scraped)