Function that returns (expt -1 (+ ?i ?j)) * determinant of the matrix less the row ?i and column ?j
(<=> (Cofactor ?M ?I ?J) (And (Square-Matrix ?M) (< 1 (Size ?M)) (Defined (Value ?M ?I ?J)) (= ?Cof (* (Expt -1 (+ ?I ?J)) (Determinant (Matrix-Less-Row-And-Column ?M ?I ?J))))))
(Nth-Domain Cofactor 1 Square-Matrix)
(=> (And (Square-Matrix ?M)) (= (Determinant ?M) (Cond ((= 1 (Size ?M)) (Value ?M 1 1)) ((< 1 (Size ?M)) (Summation (Lambda (?J) (* (Value ?M 1 ?J) (Cofactor ?M 1 ?J))) 1 (Size ?M)))))) (=> (= (Cofactor ?M ?I ?J) ?Cof) (= ?Cof (* (Expt -1 (+ ?I ?J)) (Determinant (Matrix-Less-Row-And-Column ?M ?I ?J))))) (=> (= (Cofactor ?M ?I ?J) ?Cof) (Defined (Value ?M ?I ?J))) (=> (= (Cofactor ?M ?I ?J) ?Cof) (< 1 (Size ?M))) (=> (= (Cofactor ?M ?I ?J) ?Cof) (Square-Matrix ?M))