# HG changeset patch
# User himmelma
# Date 1243518860 -7200
# Node ID 8ef7ba78bf260e5cf4d44cedb276412a456e24a8
# Parent 4ae81233cf69c57ddd89584a4347f8c0deeeaad7
corrected problem in Determinants
diff -r 4ae81233cf69 -r 8ef7ba78bf26 src/HOL/Library/Determinants.thy
--- a/src/HOL/Library/Determinants.thy Thu May 28 15:42:44 2009 +0200
+++ b/src/HOL/Library/Determinants.thy Thu May 28 15:54:20 2009 +0200
@@ -733,7 +733,7 @@
apply simp
done
from c ci
- have thr0: "- row i A = setsum (\j. (1/ c i) *s c j *s row j A) (?U - {i})"
+ have thr0: "- row i A = setsum (\j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
unfolding setsum_diff1'[OF fU iU] setsum_cmul
apply -
apply (rule vector_mul_lcancel_imp[OF ci])
@@ -1006,7 +1006,7 @@
by(simp add: norm_mul field_simps)}
moreover
{assume z: "x \ 0" "y \ 0"
- have th00: "x = norm x *s inverse (norm x) *s x" "y = norm y *s inverse (norm y) *s y" "norm x *s f (inverse (norm x) *s x) = norm x *s f (inverse (norm x) *s x)"
+ have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)"
"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)"
"norm (inverse (norm x) *s x) = 1"
"norm (f (inverse (norm x) *s x)) = 1"