equal
deleted
inserted
replaced
834 done |
834 done |
835 have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}" |
835 have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}" |
836 unfolding thr0 |
836 unfolding thr0 |
837 apply (rule span_setsum) |
837 apply (rule span_setsum) |
838 apply simp |
838 apply simp |
839 apply (rule ballI) |
|
840 apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ |
839 apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ |
841 apply (rule span_superset) |
840 apply (rule span_superset) |
842 apply auto |
841 apply auto |
843 done |
842 done |
844 let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
843 let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
876 then have thd1: "det (\<chi> i. row i A) = det A" |
875 then have thd1: "det (\<chi> i. row i A) = det A" |
877 by simp |
876 by simp |
878 have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A" |
877 have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A" |
879 apply (rule det_row_span) |
878 apply (rule det_row_span) |
880 apply (rule span_setsum) |
879 apply (rule span_setsum) |
881 apply (rule ballI) |
|
882 apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ |
880 apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ |
883 apply (rule span_superset) |
881 apply (rule span_superset) |
884 apply auto |
882 apply auto |
885 done |
883 done |
886 show "?lhs = x$k * det A" |
884 show "?lhs = x$k * det A" |