[isabelle] matrix constructions


I have a class that has the binary operations * and +, and I would like to define an instantiation of this class for matrices with the usual operations for matrices.

(A * B) i j = Sum_k (A i k) * (B k j).

The dimension of the matrices must be finite because the plus operation is binary.

Is there a way of defining this structure with the instantiation mechanism of Isabelle?

Best regards,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.