I've been reading the treatment of matrices in vectors.ml. I only need
two by two matrices for now. I don't find a procedure MATRIX_ARITH
analogous to VECTOR_ARITH or REAL_ARITH. Is there anything like that?
Here's a sample I would like to use it on.
let MATRIXTWO_MUL_COMPONENT = prove
( `!A:real^2^2 x:real^2.
(A**x)$1 = A$1$1 * x$1 + A$1$2 * x$2 /\
(A**x)$2 = A$2$1 * x$1 + A$2$2 * x$2`,
.... I don't know how to prove it. Can anyone help?
BTW, I am very thankful to all those who have helped me on this list so
far.
Michael Beeson
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
