--I have no idea what motivated this, but it is trivial to prove if by "prove" we mean, you are willing to accept probabilistic proof. I.e. using the Schwartz-Zippel lemma.
Andy Latto: I don't think so, because of the "up to a bit of messing around". In the commutative case, the "up to a bit of messing around" is "up to multiplication by some diagonal matrix. If the entries in this diagonal matrix were themselves polynomial or rational in the original 9 variables, then the Schwartz-Zippel lemma would apply, and the theorem would also be provable by any decent computer algebra system. But Schwartz-Zippel only applies to "are these two polynomials identical?", not to "are these polynomials related by a constant multiple?" WDS: the diagonals indeed have entries that are rational fns, and the MAXIMA proof below extracted from the web page Stay pointed to, proves this: M: matrix([a,b,c],[d,e,f],[g,h,i]); M1: invert(transpose(1/M)); M2: invert(transpose(1/M1)); M3: invert(transpose(1/M2)); D1: M[1,1]/M3[1,1]; D2: M[2,1]/M3[2,1]; D3: M[3,1]/M3[3,1]; D: matrix([D1,0,0],[0,D2,0],[0,0,D3]); DM3: D . M3; E1: 1; /* M[1,1] = DM3[1,1] by choice of D1 */ E2: M[1,2]/DM3[1,2]; E3: M[1,3]/DM3[1,3]; E: matrix([E1,0,0],[0,E2,0],[0,0,E3]); DM3E: DM3 . E; ratsimp(DM3E); at which point it outputs the original matrix to prove the theorem. I am just saying, Schwartz-ZIppel lemma would have done this way faster to get a probabilistic proof. -- Warren D. Smith http://RangeVoting.org <-- add your endorsement (by clicking "endorse" as 1st step)