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.
A finite square real matrix is invertible if and only if its determinant is nonzero
Statement
For every and every real matrix ,
Facts & Assumptions
Given: A real square matrix of positive finite size.
Over a field, the ring-matrix and field-matrix interfaces agree (For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface).
An RREF with fewer than pivots has a zero row; its pivot columns increase from left to right (Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns).
A square matrix is invertible exactly when its RREF is the identity, equivalently when it has pivots (Invertible matrix theorem: invertibility, full pivot rank, RREF , trivial nullspace and unique solvability are equivalent).
A row swap negates determinant, nonzero real row scaling multiplies it by a nonzero scalar, and row addition leaves it unchanged (For every square matrix, including singular ones, a row swap negates the determinant, scaling a row by any scalar scales it, and row addition leaves it unchanged).
The determinant of a triangular matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).
An invertible matrix over a commutative ring has unit determinant (An invertible square matrix over a commutative ring has unit determinant).
The real numbers form a field (The reals form a field).
Proof
If is invertible, [L1] and [L6] make a unit of , hence nonzero by [L7].
Conversely suppose is not invertible and row reduce it to its RREF . By [L3], has fewer than pivots and hence a zero row. Its pivot in row , when present, lies in a column at least , so every entry below the diagonal is zero; thus is upper triangular.
The zero row forces a zero diagonal entry, so [L5] gives .
Along the finite real row reduction, swaps and row additions preserve whether determinant is zero, and a scaling uses a nonzero scalar whose inverse gives the reverse implication. Hence .
Steps 1.2–3.1 prove the contrapositive invertible; combining it with step 1.1 proves the equivalence.
Depends on
- For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface
- Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns
- Invertible matrix theorem: invertibility, full pivot rank, RREF $I$, trivial nullspace and unique solvability are equivalent
- For every square matrix, including singular ones, a row swap negates the determinant, scaling a row by any scalar scales it, and row addition leaves it unchanged
- The determinant of a triangular matrix is the product of its diagonal entries
- An invertible square matrix over a commutative ring has unit determinant
- The reals form a field
Used by
- Conjugation and the adjoint representation of a Lie group Definition
- A matrix has rank at least r exactly when it has a nonzero r-rowed minor Lemma
- A nonzero rank minor supplies the source coordinates for the constant-rank theorem Lemma
- Change of variables for a C¹ map injective and regular only on the interior of a compact Jordan set Lemma
- A fibrewise bijective smooth bundle map over a diffeomorphism is a bundle isomorphism Proposition
- A linear endomorphism of ℝⁿ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant Theorem
- A linear map T of ℝⁿ sends Lebesgue measurable sets to Lebesgue measurable sets, with λₙ(T[E])=|det T| λₙ(E) when T is invertible and T[E] Lebesgue null when it is not Theorem
- Dual and Hom transition functions define smooth bundles Theorem
Dependency tree · two levels
38 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
- D. Margalit and J. Rabinoff, Interactive Linear Algebra, §4.1, Invertibility Property (standard reference, not scraped)