Generalize trace_mult_sym to square products of non-square matrices.

--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Jun 25 20:38:06 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Jun 25 17:13:09 2013 -0500
@@ -84,7 +84,7 @@
 lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
   by (simp add: trace_def setsum_subtractf)
 
-lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)"
+lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
   apply (simp add: trace_def matrix_matrix_mult_def)
   apply (subst setsum_commute)
   by (simp add: mult_commute)