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"