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.
FALSE: a square matrix over a commutative ring is invertible if and only if its determinant is nonzero
Statement
False claim: for every commutative ring and every positive-sized square matrix over , the matrix is invertible if and only if .
Facts & Assumptions
Given: The claimed equivalence over arbitrary commutative rings.
A ring in the published convention may be the zero ring (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).
is a commutative ring (The integers form a commutative ring) and its only units are and ( is a commutative monoid whose group of units is ; equivalently holds exactly for and ).
For a positive-sized square matrix over a commutative ring, (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
The correct general criterion is: a positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit (A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit).
Refutation
The reverse implication fails in . By [F3], the unique term in the determinant gives . This determinant is nonzero but is not a unit by [F2], so [L1] shows that is not invertible.
The forward implication also fails under the stated ring convention. In the zero ring allowed by [F1], the identity matrix is ; it is its own two-sided inverse, and [F3] gives its determinant as .
Thus both directions of the claimed equivalence can fail. Replacing "nonzero" by "a unit" gives the valid equivalence [L1], including for the zero ring.
Depends on
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit
- Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides
- The integers form a commutative ring
- $(\mathbb{Z}, \cdot, 1)$ is a commutative monoid whose group of units is $\{1, -1\}$; equivalently $u \mid 1$ holds exactly for $u = 1$ and $u = -1$
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: 100 results over 26 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
- András Pál, Introduction to Commutative Algebra, Proposition 7.2 (standard reference, not scraped)