let n be Nat; :: thesis: for K being Field
for M being Matrix of n,K st Det M <> 0. K holds
M ~ = ((Det M) " ) * ((Matrix_of_Cofactor M) @ )
let K be Field; :: thesis: for M being Matrix of n,K st Det M <> 0. K holds
M ~ = ((Det M) " ) * ((Matrix_of_Cofactor M) @ )
let M be Matrix of n,K; :: thesis: ( Det M <> 0. K implies M ~ = ((Det M) " ) * ((Matrix_of_Cofactor M) @ ) )
set C = ((Det M) " ) * ((Matrix_of_Cofactor M) @ );
assume A1: Det M <> 0. K ; :: thesis: M ~ = ((Det M) " ) * ((Matrix_of_Cofactor M) @ )
then ( (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) * M = 1. K,n & M * (((Det M) " ) * ((Matrix_of_Cofactor M) @ )) = 1. K,n ) by Th30, Th33;
then ( M is invertible & M is_reverse_of ((Det M) " ) * ((Matrix_of_Cofactor M) @ ) ) by A1, Th34, MATRIX_6:def 2;
hence M ~ = ((Det M) " ) * ((Matrix_of_Cofactor M) @ ) by MATRIX_6:def 4; :: thesis: verum