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.
Invertible matrices and the general linear group
Definition
A matrix is invertible when there is a matrix such that
Such a is unique and is denoted . The general linear set is
It is the set of units of the ring . The fact that it is a group under matrix multiplication is is a group under matrix multiplication, including the trivial group ↗. For , the unique empty matrix is and is its own inverse.
Depends on
Used by
- Every elementary matrix is invertible, with inverse given by the reverse elementary operation Corollary
- GLₙ(F) is a group under matrix multiplication, including the trivial group GL₀(F) Corollary
- Similar matrices have the same trace Corollary
- Similar matrices: B=P⁻¹AP for an invertible P Definition
- For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface Proposition
- [v]_mathcal C=P_mathcal C←mathcal B[v]_mathcal B and P_mathcal B←mathcal C=P_mathcal C←mathcal B⁻¹ Theorem
- A square matrix is invertible exactly when its multiplication map is a linear isomorphism; matrices preserve inverses of linear isomorphisms Theorem
- Invertible matrix theorem: invertibility, full pivot rank, RREF I, trivial nullspace and unique solvability are equivalent Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 24 results over 13 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. Axler, Linear Algebra Done Right, 4th ed., Definition 3.80 (standard reference, not scraped)
- S. Schiavone, MIT 18.700 Day 9, Definition 33 (standard reference, not scraped)