There is a matrix multiplication definition in Cartesian_Euclidean_Space
(in directory HOL/Multivariate_Analysis"):
definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m ⇒ 'a ^'p^'n ⇒ 'a ^ 'p ^'m"
(infixl "**" 70)
where "m ** m' == (χ i j. setsum (λk. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
Now the the squared matrix would be A ** A
and A^3 would be A ** A ** A
.
I couldn't find a powerfunction, to define A^n
(i.e., A ** A ** ... ** A
n times).
Is there a power function in the library? Is a manual definition needed?