description/proof of that over field, square matrix has inverse iff its determinant is nonzero, and inverse is this
Topics
About: matrices space
The table of contents of this article
Starting Context
- The reader knows a definition of determinant of square matrix over ring.
- The reader knows a definition of inverse of square matrix over ring.
- The reader admits the proposition that over any commutative ring, the determinant of the product of any square matrices is the product of the determinants of the matrices.
- The reader admits the Laplace expansion of the determinant of any square matrix over any commutative ring holds and its corollary.
Target Context
- The reader will have a description and a proof of the proposition that over any field, any square matrix has the inverse if and only if its determinant is nonzero, and the inverse is this.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(F\): \(\in \{\text{ the fields }\}\)
\(n\): \(\in \mathbb{N} \setminus \{0\}\)
\(M\): \(\in \{\text{ the } n \times n R \text{ matrices }\}\)
//
Statements:
(
\(det M \neq 0\)
\(\iff\)
\(\exists M^{-1}\)
)
\(\land\)
(
\(\exists M^{-1}\)
\(\implies\)
\({M^{-1}}^j_l = 1 / det M M_{l, j}\)
)
//
2: Proof
Whole Strategy: Step 1: suppose that \(M^{-1}\) exists, and see that \(det M \neq 0\); Step 2: suppose that \(det M \neq 0\), and see that \(M^{-1}\) exists by seeing that \({M^{-1}}^j_l = 1 / det M M_{l, j}\).
Step 1:
Let us suppose that \(M^{-1}\) exists.
\(M M^{-1} = I\).
\(det (M M^{-1}) = det I = 1\), but \(det (M M^{-1}) = det M det M^{-1}\), by the proposition that over any commutative ring, the determinant of the product of any square matrices is the product of the determinants of the matrices.
So, \(det M \neq 0\).
Step 2:
Let us suppose that \(det M \neq 0\).
By the Laplace expansion of the determinant of any square matrix over any commutative ring holds and its corollary, \(det M \delta^j_{j'} = \sum_{l \in \{1, ..., m\}} M^j_l M_{j', l}\) and \(det M \delta^l_{l'} = \sum_{j \in \{1, ..., m\}} M^j_l M_{j, l'}\).
That means that \({M^{-1}}^j_l = 1 / det M M_{l, j}\), so, \(M^{-1}\) exists.
