ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-11

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.

One matrix has two distinct row echelon forms but one reduced row echelon form

Example

Over $Q$ , the matrix $A = (\begin{array}{cc} 1 & 1 \\ 1 & 0 \end{array})$ has distinct row echelon forms $R = (\begin{array}{cc} 1 & 1 \\ 0 & - 1 \end{array}), S = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array}),$ but both reduce to $I_{2}$ .

Facts & Assumptions

Given: The displayed matrix and two proposed reductions.

[L1]

Every finite matrix over a field is row equivalent to exactly one matrix in reduced row echelon form (Every finite matrix over a field is row equivalent to exactly one reduced row echelon matrix).

[L2]

A matrix is in row echelon form when every zero row lies below every nonzero row, the leading entry — the leftmost nonzero entry — of each nonzero row lies strictly to the right of the leading entry in the row above it, and every entry below a leading entry is zero. A row echelon matrix is in reduced row echelon form when every leading entry equals $1$ and is the only nonzero entry in its column (Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns).

[L3]

Over a field $F$ , an elementary row operation interchanges two distinct rows, replaces $R_{p}$ by $c R_{p}$ for a nonzero $c \in F$ , or replaces $R_{p}$ by $R_{p} + c R_{q}$ for distinct $p, q$ and $c \in F$ ; two matrices are row equivalent when a finite sequence of elementary row operations transforms one into the other (Elementary row operations and row equivalence for finite matrices over a field).

Verification

technique · direct

1.1

The replacement $R_{1} \leftarrow R_{1} + (- 1) R_{0}$ is an elementary row operation of the third kind and takes $A$ to $R$ ; the scaling $R_{1} \leftarrow (- 1) R_{1}$ is one of the second kind, $- 1$ being nonzero in $Q$ , and takes $R$ to $S$ . So $A$ is row equivalent to each of $R$ and $S$ by [L3]. Each has no zero row, leading entries in columns $0$ and $1$ respectively, and $0$ below the leading entry of its first row, so each is in row echelon form by [L2]. Finally $R \neq S$ because $- 1 \neq 1$ in $Q$ . The ground field matters here and not elsewhere in the example: over $F_{2}$ one has $- 1 = 1$ , so $R$ and $S$ coincide and this matrix exhibits no failure of uniqueness.

L2L3algebra

2.1

From $S$ , the replacement $R_{0} \leftarrow R_{0} + (- 1) R_{1}$ is again elementary of the third kind and gives $I_{2}$ , so $I_{2}$ is row equivalent to $A$ by [L3] and step 1.1; its two leading entries equal $1$ and each is alone in its column, so it is in reduced row echelon form by [L2]. Applying the same replacement after the scaling of step 1.1 carries $R$ to $I_{2}$ as well, in agreement with the uniqueness of [L1].

step 1.1L1L2L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

J. Hefferon, Linear Algebra, 4th ed., Ch. One, §III.2 (standard reference, not scraped)