Class INVERTIBLE-MATRIX

• Defined in theory: Basic-matrix-algebra
• Source code: basic-matrix.lisp

Slots on this class:

Documentation:

Class of the matrices that can be inverted

Instance-Of: Class

Subclass-Of: Square-matrix

Domain-Of: Matrix-inverse

Range-Of: Matrix-inverse

Equivalence Axioms:

(<=> (Invertible-Matrix ?M)
     (And (Square-Matrix ?M) (Not (Zero-Element (Determinant ?M)))))

Axioms:

(Not (Zero-Element (Determinant ?M)))

(Square-Matrix ?M)

Other Related Axioms:

(<=> (Invertible-Matrix ?M)
     (And (Square-Matrix ?M)
          (Exists (?M-1)
                  (And (Square-Matrix ?M-1)
                       (Identity-Matrix (* ?M ?M-1))
                       (Identity-Matrix (* ?M-1 ?M))))))

(<=> (Invertible-Matrix ?M)
     (And (Square-Matrix ?M) (Not (Zero-Element (Determinant ?M)))))

(=> (Matrix-Inverse $X $Y) (Invertible-Matrix $Y))

(=> (Matrix-Inverse $X $Y) (Invertible-Matrix $X))

(=> (= (Matrix-Inverse ?M) ?M-1) (Invertible-Matrix ?M-1))

(=> (= (Matrix-Inverse ?M) ?M-1) (Invertible-Matrix ?M))