Hi Abid,
| 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.
I think the following should work --- I should probably add it to the system
as it might be useful for
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 d
