src/HOL/Analysis/Determinants.thy
changeset 66804 3f9bb52082c4
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Analysis/Determinants.thy	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Determinants.thy	Sun Oct 08 22:28:20 2017 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
     1.6    apply (simp add: trace_def matrix_matrix_mult_def)
     1.7 -  apply (subst sum.commute)
     1.8 +  apply (subst sum.swap)
     1.9    apply (simp add: mult.commute)
    1.10    done
    1.11