src/HOL/Library/Determinants.thy
changeset 31280 8ef7ba78bf26
parent 30843 3419ca741dbf
child 31291 a2f737a72655
equal deleted inserted replaced
31279:4ae81233cf69 31280:8ef7ba78bf26
   731       apply (drule_tac f="op + (- a)" in cong[OF refl])
   731       apply (drule_tac f="op + (- a)" in cong[OF refl])
   732       apply (simp only: ab_left_minus add_assoc[symmetric])
   732       apply (simp only: ab_left_minus add_assoc[symmetric])
   733       apply simp
   733       apply simp
   734       done
   734       done
   735     from c ci
   735     from c ci
   736     have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s c j *s row j A) (?U - {i})"
   736     have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
   737       unfolding setsum_diff1'[OF fU iU] setsum_cmul
   737       unfolding setsum_diff1'[OF fU iU] setsum_cmul
   738       apply -
   738       apply -
   739       apply (rule vector_mul_lcancel_imp[OF ci])
   739       apply (rule vector_mul_lcancel_imp[OF ci])
   740       apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps)
   740       apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps)
   741       unfolding stupid ..
   741       unfolding stupid ..
  1004 	apply (simp add: dist_def norm_mul)
  1004 	apply (simp add: dist_def norm_mul)
  1005 	apply (rule f1[rule_format])
  1005 	apply (rule f1[rule_format])
  1006 	by(simp add: norm_mul field_simps)}
  1006 	by(simp add: norm_mul field_simps)}
  1007     moreover
  1007     moreover
  1008     {assume z: "x \<noteq> 0" "y \<noteq> 0"
  1008     {assume z: "x \<noteq> 0" "y \<noteq> 0"
  1009       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)"
  1009       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)"
  1010 	"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)"
  1010 	"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)"
  1011 	"norm (inverse (norm x) *s x) = 1"
  1011 	"norm (inverse (norm x) *s x) = 1"
  1012 	"norm (f (inverse (norm x) *s x)) = 1"
  1012 	"norm (f (inverse (norm x) *s x)) = 1"
  1013 	"norm (inverse (norm y) *s y) = 1"
  1013 	"norm (inverse (norm y) *s y) = 1"
  1014 	"norm (f (inverse (norm y) *s y)) = 1"
  1014 	"norm (f (inverse (norm y) *s y)) = 1"