CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Row reducing $[A\mid I]$ yields $[I\mid A^{-1}]$ exactly when $A$ is invertible

Statement

For $A\in M_n(F)$ , row reduction of $[A\mid I_n]$ can reach $[I_n\mid B]$ if and only if $A$ is invertible. Whenever it does, $B=A^{-1}$ .

Facts & Assumptions

Given: A square matrix $A$ over a field and a finite row reduction of $[A\mid I_n]$ .

[L1]

$A$ is invertible exactly when its RREF is $I_n$ (Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent).

[L2]

Each row operation is simultaneous left multiplication on both blocks by its elementary matrix (Applying an elementary row operation is left multiplication by its elementary matrix).

[L3]

A whole reduction is encoded by one product $E$ of elementary matrices (A finite row reduction from $A$ to $B$ is encoded by $B=E_r\cdots E_1A$ ).

[L4]

An augmented matrix records simultaneous row operations on all its columns (Matrix equation $Ax=b$ , its solution set, consistency, homogeneous systems and the augmented matrix $[A\mid b]$ ).

Proof

technique · constructive

1.1

Let $E$ be the product encoding the row operations. The two output blocks are $EA$ and $EI_n=E$ .

L2L3L4construct

2.1

If the output is $[I_n\mid B]$ , then $EA=I_n$ and $B=E$ . By [L1], $A$ is invertible, and multiplying $EA=I_n$ by $A^{-1}$ gives $E=A^{-1}=B$ .

step 1.1L1algebra

3.1

Conversely, if $A$ is invertible, [L1] supplies a reduction of $A$ to $I_n$ ; applying it to $[A\mid I_n]$ gives $[I_n\mid A^{-1}]$ by step 2.1. If the left block cannot reach $I_n$ , [L1] says no inverse exists.

step 2.1L1discharge-construct∎

Depends on

Used by

A 3×3 inverse computed by row reducing [A∣ I] Example

Dependency tree · next 3 levels

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

D. Margalit and J. Rabinoff, Interactive Linear Algebra, §3.6 (standard reference, not scraped)

Row reducing [A∣I][A\mid I][A∣I] yields [I∣A−1][I\mid A^{-1}][I∣A−1] exactly when AAA is invertible