src/HOL/Library/Determinants.thy
 changeset 31280 8ef7ba78bf26 parent 30843 3419ca741dbf child 31291 a2f737a72655
```     1.1 --- a/src/HOL/Library/Determinants.thy	Thu May 28 15:42:44 2009 +0200
1.2 +++ b/src/HOL/Library/Determinants.thy	Thu May 28 15:54:20 2009 +0200
1.3 @@ -733,7 +733,7 @@
1.4        apply simp
1.5        done
1.6      from c ci
1.7 -    have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s c j *s row j A) (?U - {i})"
1.8 +    have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
1.9        unfolding setsum_diff1'[OF fU iU] setsum_cmul
1.10        apply -
1.11        apply (rule vector_mul_lcancel_imp[OF ci])
1.12 @@ -1006,7 +1006,7 @@
1.13  	by(simp add: norm_mul field_simps)}
1.14      moreover
1.15      {assume z: "x \<noteq> 0" "y \<noteq> 0"
1.16 -      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)"
1.17 +      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)"
1.18  	"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)"
1.19  	"norm (inverse (norm x) *s x) = 1"
1.20  	"norm (f (inverse (norm x) *s x)) = 1"
```