equal
deleted
inserted
replaced
284 and r: "row i A = row j A" |
284 and r: "row i A = row j A" |
285 shows "det A = 0" |
285 shows "det A = 0" |
286 proof- |
286 proof- |
287 have tha: "\<And>(a::'a) b. a = b ==> b = - a ==> a = 0" |
287 have tha: "\<And>(a::'a) b. a = b ==> b = - a ==> a = 0" |
288 by simp |
288 by simp |
289 have th1: "of_int (-1) = - 1" by (metis of_int_1 of_int_minus number_of_Min) |
289 have th1: "of_int (-1) = - 1" by simp |
290 let ?p = "Fun.swap i j id" |
290 let ?p = "Fun.swap i j id" |
291 let ?A = "\<chi> i. A $ ?p i" |
291 let ?A = "\<chi> i. A $ ?p i" |
292 from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def) |
292 from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def) |
293 hence "det A = det ?A" by simp |
293 hence "det A = det ?A" by simp |
294 moreover have "det A = - det ?A" |
294 moreover have "det A = - det ?A" |
1056 have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto |
1056 have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto |
1057 show ?thesis |
1057 show ?thesis |
1058 unfolding det_def UNIV_2 |
1058 unfolding det_def UNIV_2 |
1059 unfolding setsum_over_permutations_insert[OF f12] |
1059 unfolding setsum_over_permutations_insert[OF f12] |
1060 unfolding permutes_sing |
1060 unfolding permutes_sing |
1061 apply (simp add: sign_swap_id sign_id swap_id_eq) |
1061 by (simp add: sign_swap_id sign_id swap_id_eq) |
1062 by (simp add: arith_simps(31)[symmetric] del: arith_simps(31)) |
|
1063 qed |
1062 qed |
1064 |
1063 |
1065 lemma det_3: "det (A::'a::comm_ring_1^3^3) = |
1064 lemma det_3: "det (A::'a::comm_ring_1^3^3) = |
1066 A$1$1 * A$2$2 * A$3$3 + |
1065 A$1$1 * A$2$2 * A$3$3 + |
1067 A$1$2 * A$2$3 * A$3$1 + |
1066 A$1$2 * A$2$3 * A$3$1 + |
1077 unfolding det_def UNIV_3 |
1076 unfolding det_def UNIV_3 |
1078 unfolding setsum_over_permutations_insert[OF f123] |
1077 unfolding setsum_over_permutations_insert[OF f123] |
1079 unfolding setsum_over_permutations_insert[OF f23] |
1078 unfolding setsum_over_permutations_insert[OF f23] |
1080 |
1079 |
1081 unfolding permutes_sing |
1080 unfolding permutes_sing |
1082 apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) |
1081 by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) |
1083 apply (simp add: arith_simps(31)[symmetric] del: arith_simps(31)) |
|
1084 by (simp add: field_simps) |
|
1085 qed |
1082 qed |
1086 |
1083 |
1087 end |
1084 end |