# Is there a proof that a matrix is invertible iff its determinant is non-zero which doesn't presuppose the formula for the determinant?

Proofs of the fact that a matrix is invertible iff its determinant is non-zero generally begin by saying "Define the determinant to be [very complicated formula]. We will now prove the result...". This is obviously unsatisfactory to many people.

Other proofs begin by listing axioms that the determinant should verify, and then prove that such a function exists (and is unique) and is given by the given formula. This isn't much better - why should we be interested in these axioms? Without knowing better, there isn't even any reason to suspect there exists any polynomial or simple function at all such that $f(A)=0$ iff $A$ is singular.

If you apply Gaussian elimination to a general 2x2 or 3x3 matrix, you get tantalizingly close, because the determinant formula arises naturally from the calculations, and it's clear that indeed, if it's zero, the matrix must be invertible. The trouble is that in order to get to that point, you need to start assuming that this, that and the other is non-zero so that you can divide by them, and your assumptions begin branching: if that's non-zero, then assume this is non-zero, otherwise... So it's difficult to see how this could be turned into a proper proof.

Can the proof outlined in the last paragraph be carried out rigorously? Or something like it?

• The problem is, we have to define the determinant somehow. The closest you can get, as far as I know, to what you outline is the axiomatic approach. In fact, you can quite easily show that so defined determinant needs to be unique, but again, you somehow need to prove that determinant satisfying these properties exists. – Wojowu Sep 9 '16 at 18:31
• @Wojowu That seems to me like saying "The problem is, to prove $1 + 2 + ... + n$ is equal to a quadratic in $n$, we need to define that quadratic somehow." No we don't - any of the direct proofs simultaneously prove that a quadratic exists, and tell you what it is, without ever requiring you to conjecture anything about the eventual nature of the answer. Like I said, an analysis of Gaussian elimination almost gets you there, if you could just find a way to tame the branching cases. – Jack M Sep 9 '16 at 18:42
• @Jack: you can perform Gaussian elimination in the fraction field of the polynomial ring on each entry, treating them as indeterminates. Then you you don't need to keep track of any assumptions about things being nonzero. The key fact here is that polynomial rings are integral domains. More geometrically, whenever you assume that something is nonzero you're restricting yourself to a Zariski open subset of matrices, but Zariski opens are dense here so it's not a problem. – Qiaochu Yuan Sep 9 '16 at 19:16
• Jack, I think @Wojowu is saying that the question doesn't even make sense without a definition of the determinant of a matrix. So what is your definition? Any proof will depend very much on your choice. – TonyK Sep 9 '16 at 19:22
• QiaochuYuan's answer references Axler's book on linear algebra, and that text is avowedly written in a determinant-free manner. For shorter reading, see also Axler's paper "Down with Determinants" by Axler and this n-Category Cafe post. – Semiclassical Sep 9 '16 at 19:24

Let me work over the complex numbers. You can take the approach which I think is described in Axler: show that every square matrix over $\mathbb{C}$ can be upper triangularized (which can be done cleanly and conceptually: once you know that eigenvectors exist, just repeatedly find them and quotient by them), and define the determinant to be the product of the diagonal entries of an upper triangularization. Show that this doesn't depend on the choice of upper triangularization. Now it's very easy to check that an upper triangular matrix is invertible iff its diagonal entries are nonzero.
• @Qiaochau Yuan. My first reflex to show that an eigenvector exist is to say that the characteristic polynomial has a root (in $\mathbb{C}$), an eigenvalue. But the simplest definition I know of the characteristic polynomial involves the determinant. How do you bypass this? – A.B. Sep 9 '16 at 19:52
• @Amadou: let $M$ be an $n \times n$ matrix. The space of such matrices is $n^2$ dimensional, so the matrices $\{ 1, M, M^2, \dots M^{n^2} \}$ are linearly dependent. This means $M$ satisfies some polynomial equation (not necessarily the characteristic polynomial) and from here the proof is as usual assuming FTA. There are also direct proofs that avoid (and hence prove!) FTA. – Qiaochu Yuan Sep 9 '16 at 19:55