TheoremStatement: Literature-sourcedProof: 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.

Every nonzero commutative ring has invariant basis number for finite bases

Statement

Every nonzero commutative unital ring has invariant basis number for finite bases: if $R^{m} ≅ R^{n}$ as $R$ -modules, then $m = n$ . The proof is choice-free.

Facts & Assumptions

Given: A nonzero commutative unital ring $R$ and inverse module isomorphisms $R^{m} ⇄ R^{n}$ .

[F1]

Invariant basis number means precisely that $R^{m} ≅ R^{n}$ forces $m = n$ for finite $m, n$ (Invariant basis number and the rank of a free module).

[F2]

Rectangular matrix products use $(A B)_{i k} = \sum_{j} a_{i j} b_{j k}$ ; matrix multiplication is associative and the identity matrices are multiplicative identities, including for zero-sized shapes (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose, Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products).

[F4]

The module $R^{n}$ is free on its standard coordinate vectors, and every vector has a unique finite coordinate expression (The free module on a set and its standard basis).

[F3]

The determinant of an $n \times n$ matrix over a commutative ring is normalized and multilinear in its columns (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, The determinant is the unique normalized alternating multilinear function on the columns).

[L1]

An $n \times n$ matrix with a zero column or two equal columns has determinant zero (A square matrix with a zero column or two equal columns has determinant zero).

Proof

technique · contradiction

1.1

Record the images of the standard basis vectors from [F4] as the columns of rectangular matrices $A$ and $B$ . The coordinate formula and [F2] turn the two inverse composites into $A B = I_{n}$ and $B A = I_{m}$ .

givenF2F4

2.1

Suppose first that $n > m$ . Each of the $n$ columns of $A B$ is an $R$ -linear combination of the $m$ columns of $A$ .

assume-contrastep 1.1F2

3.1

Expanding $\det (A B)$ by multilinearity in all $n$ columns, each term chooses one of the $m$ columns of $A$ in each of $n$ positions. Since $n > m$ , some chosen column repeats, so every term is zero by [L1]. Thus $\det (A B) = 0$ .

step 2.1F3L1

4.1

But $A B = I_{n}$ , so normalization gives $\det (A B) = 1_{R} \neq 0$ , contradicting step 3.1. Hence $n \leq m$ .

step 1.1step 3.1F3

5.1

Interchanging $A, B$ and $m, n$ gives $m \leq n$ . Therefore $m = n$ , proving [F1]. The cases $m = 0$ or $n = 0$ are included: a strict inequality makes the other positive and the same determinant argument applies.

step 4.1F1discharge-contradiction∎

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: 75 results over 14 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

A. Kleshchev, Lectures on Abstract Algebra for Graduate Students, sections 3.6, 3.14, and 3.15 (standard reference, not scraped)
The Stacks Project, Algebra (standard reference, not scraped)
P. Hekmati, Homological Algebra, section 3.1 (standard reference, not scraped)