Alphabeta MathHow 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.
An invertible square matrix over a commutative ring has unit determinant
Statement
Let . If is invertible over a commutative ring, then is a unit of . More precisely, is its inverse.
Facts & Assumptions
Given: An invertible matrix with inverse .
Determinants multiply: (For same-sized finite square matrices over a commutative ring, ).
A unit is an element with a two-sided multiplicative inverse, and its inverse is unique (The units of a ring are the invertible elements of its multiplicative monoid, and is a group under multiplication; only in the zero ring).
Identity matrices are multiplicative identities (Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products).
Matrix invertibility gives (Invertible square matrices and similarity over a commutative ring).
The determinant is normalized: (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).
Proof
Apply [L1] to the two equations in [L4]: and .
Thus is a unit with inverse by [L2]. In the zero ring, and the same two-sided equation still gives the unit conclusion.
Depends on
- Invertible square matrices and similarity over a commutative ring
- For same-sized finite square matrices over a commutative ring, $\det(AB)=\det(A)\det(B)$
- The units of a ring are the invertible elements of its multiplicative monoid, and $R^{\times}$ is a group under multiplication; $0 \in R^{\times}$ only in the zero ring
- Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products
- The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring
Used by
- If A is invertible over a commutative ring, then det(A⁻¹)=det(A)⁻¹ Corollary
- An integer matrix of determinant 2 is invertible over ℚ but not over ℤ Example
- For n≥ 1, determinant is a natural transformation det:GLₙ(-)⟹(-)^× from commutative rings to groups Example
- Row operations track determinant correctly for a singular triangular matrix over ℤ/6 Example
- A finite square real matrix is invertible if and only if its determinant is nonzero Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 46 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
- S. New, MATH 146 Linear Algebra 1 Lecture Notes, Theorem 4.24 (standard reference, not scraped)