# 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"