# HG changeset patch
# User Stephen W. Nuchia
# Date 1372198389 18000
# Node ID e64c1344f21b48b82bbea6890e6f6f908bb19d0e
# Parent  e09e1091394d74aec9bdb48e2df39c41301f0bd0
Generalize trace_mult_sym to square products of non-square matrices.

diff -r e09e1091394d -r e64c1344f21b src/HOL/Multivariate_Analysis/Determinants.thy
--- 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)