Dear All,
I have a Query about Matrices. Can i write a definition in HOL light which
takes two matrices of dimensions real^N^M and real^Q^P and after a certain
operation output a vector with dimension real^(N*Q)^(M*P).
I was going through the theory and found finite_sum, which is the addition
of dimensions, but here i need product or multiplication of dimensions. Can
anyone help me out please.
Best Regards,
Abid Rauf
Ph.D Scholar (CS) & RA SAVe Labs,
School of Electrical Engineering and Computer Science (SEECS),
National University of Science and Technology (NUST), H-12, Islamabad,
Pakistan
------------------------------------------------------------------------------
Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
