author | huffman |
Thu, 19 Feb 2009 09:42:23 -0800 | |
changeset 29993 | 84b2c432b94a |
parent 29846 | 57dccccc37b3 |
child 30041 | 9becd197a40e |
permissions | -rw-r--r-- |
29846
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1 |
(* Title: Determinants |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
2 |
ID: $Id: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
3 |
Author: Amine Chaieb, University of Cambridge |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
4 |
*) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
5 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
6 |
header {* Traces, Determinant of square matrices and some properties *} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
7 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
8 |
theory Determinants |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
9 |
imports Euclidean_Space Permutations |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
10 |
begin |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
11 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
12 |
subsection{* First some facts about products*} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
13 |
lemma setprod_insert_eq: "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
14 |
apply clarsimp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
15 |
by(subgoal_tac "insert a A = A", auto) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
16 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
17 |
lemma setprod_add_split: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
18 |
assumes mn: "(m::nat) <= n + 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
19 |
shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
20 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
21 |
let ?A = "{m .. n+p}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
22 |
let ?B = "{m .. n}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
23 |
let ?C = "{n+1..n+p}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
24 |
from mn have un: "?B \<union> ?C = ?A" by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
25 |
from mn have dj: "?B \<inter> ?C = {}" by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
26 |
have f: "finite ?B" "finite ?C" by simp_all |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
27 |
from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
28 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
29 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
30 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
31 |
lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
32 |
apply (rule setprod_reindex_cong[where f="op + p"]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
33 |
apply (auto simp add: image_iff Bex_def inj_on_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
34 |
apply arith |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
35 |
apply (rule ext) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
36 |
apply (simp add: add_commute) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
37 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
38 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
39 |
lemma setprod_singleton: "setprod f {x} = f x" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
40 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
41 |
lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
42 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
43 |
lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
44 |
"setprod f {m .. Suc n} = (if m \<le> Suc n then f (Suc n) * setprod f {m..n} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
45 |
else setprod f {m..n})" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
46 |
by (auto simp add: atLeastAtMostSuc_conv) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
47 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
48 |
lemma setprod_le: assumes fS: "finite S" and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (g x :: 'a::ordered_idom)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
49 |
shows "setprod f S \<le> setprod g S" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
50 |
using fS fg |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
51 |
apply(induct S) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
52 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
53 |
apply auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
54 |
apply (rule mult_mono) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
55 |
apply (auto intro: setprod_nonneg) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
56 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
57 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
58 |
(* FIXME: In Finite_Set there is a useless further assumption *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
59 |
lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_by_zero, field})" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
60 |
apply (erule finite_induct) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
61 |
apply (simp) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
62 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
63 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
64 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
65 |
lemma setprod_le_1: assumes fS: "finite S" and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (1::'a::ordered_idom)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
66 |
shows "setprod f S \<le> 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
67 |
using setprod_le[OF fS f] unfolding setprod_1 . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
68 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
69 |
subsection{* Trace *} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
70 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
71 |
definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
72 |
"trace A = setsum (\<lambda>i. ((A$i)$i)) {1..dimindex(UNIV::'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
73 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
74 |
lemma trace_0: "trace(mat 0) = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
75 |
by (simp add: trace_def mat_def Cart_lambda_beta setsum_0) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
76 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
77 |
lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(dimindex(UNIV::'n set))" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
78 |
by (simp add: trace_def mat_def Cart_lambda_beta) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
79 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
80 |
lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
81 |
by (simp add: trace_def setsum_addf Cart_lambda_beta vector_component) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
82 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
83 |
lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
84 |
by (simp add: trace_def setsum_subtractf Cart_lambda_beta vector_component) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
85 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
86 |
lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
87 |
apply (simp add: trace_def matrix_matrix_mult_def Cart_lambda_beta) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
88 |
apply (subst setsum_commute) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
89 |
by (simp add: mult_commute) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
90 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
91 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
92 |
(* Definition of determinant. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
93 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
94 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
95 |
definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
96 |
"det A = setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) {1 .. dimindex(UNIV :: 'n set)}) {p. p permutes {1 .. dimindex(UNIV :: 'n set)}}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
97 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
98 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
99 |
(* A few general lemmas we need below. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
100 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
101 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
102 |
lemma Cart_lambda_beta_perm: assumes p: "p permutes {1..dimindex(UNIV::'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
103 |
and i: "i \<in> {1..dimindex(UNIV::'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
104 |
shows "Cart_nth (Cart_lambda g ::'a^'n) (p i) = g(p i)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
105 |
using permutes_in_image[OF p] i |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
106 |
by (simp add: Cart_lambda_beta permutes_in_image[OF p]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
107 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
108 |
lemma setprod_permute: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
109 |
assumes p: "p permutes S" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
110 |
shows "setprod f S = setprod (f o p) S" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
111 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
112 |
{assume "\<not> finite S" hence ?thesis by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
113 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
114 |
{assume fS: "finite S" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
115 |
then have ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
116 |
apply (simp add: setprod_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
117 |
apply (rule ab_semigroup_mult.fold_image_permute) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
118 |
apply (auto simp add: p) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
119 |
apply unfold_locales |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
120 |
done} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
121 |
ultimately show ?thesis by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
122 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
123 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
124 |
lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
125 |
by (auto intro: setprod_permute) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
126 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
127 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
128 |
(* Basic determinant properties. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
129 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
130 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
131 |
lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
132 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
133 |
let ?di = "\<lambda>A i j. A$i$j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
134 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
135 |
have fU: "finite ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
136 |
{fix p assume p: "p \<in> {p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
137 |
from p have pU: "p permutes ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
138 |
have sth: "sign (inv p) = sign p" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
139 |
by (metis sign_inverse fU p mem_def Collect_def permutation_permutes) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
140 |
from permutes_inj[OF pU] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
141 |
have pi: "inj_on p ?U" by (blast intro: subset_inj_on) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
142 |
from permutes_image[OF pU] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
143 |
have "setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
144 |
also have "\<dots> = setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
145 |
unfolding setprod_reindex[OF pi] .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
146 |
also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
147 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
148 |
{fix i assume i: "i \<in> ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
149 |
from i permutes_inv_o[OF pU] permutes_in_image[OF pU] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
150 |
have "((\<lambda>i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
151 |
unfolding transp_def by (simp add: Cart_lambda_beta expand_fun_eq)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
152 |
then show "setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
153 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
154 |
finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
155 |
by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
156 |
then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
157 |
apply (rule setsum_cong2) by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
158 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
159 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
160 |
lemma det_lowerdiagonal: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
161 |
fixes A :: "'a::comm_ring_1^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
162 |
assumes ld: "\<And>i j. i \<in> {1 .. dimindex (UNIV:: 'n set)} \<Longrightarrow> j \<in> {1 .. dimindex(UNIV:: 'n set)} \<Longrightarrow> i < j \<Longrightarrow> A$i$j = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
163 |
shows "det A = setprod (\<lambda>i. A$i$i) {1..dimindex(UNIV:: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
164 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
165 |
let ?U = "{1..dimindex(UNIV:: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
166 |
let ?PU = "{p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
167 |
let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) {1 .. dimindex(UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
168 |
have fU: "finite ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
169 |
from finite_permutations[OF fU] have fPU: "finite ?PU" . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
170 |
have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
171 |
{fix p assume p: "p \<in> ?PU -{id}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
172 |
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
173 |
from permutes_natset_le[OF pU] pid obtain i where |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
174 |
i: "i \<in> ?U" "p i > i" by (metis not_le) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
175 |
from permutes_in_image[OF pU] i(1) have piU: "p i \<in> ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
176 |
from ld[OF i(1) piU i(2)] i(1) have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
177 |
from setprod_zero[OF fU ex] have "?pp p = 0" by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
178 |
then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
179 |
from setsum_superset[OF fPU id0 p0] show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
180 |
unfolding det_def by (simp add: sign_id) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
181 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
182 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
183 |
lemma det_upperdiagonal: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
184 |
fixes A :: "'a::comm_ring_1^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
185 |
assumes ld: "\<And>i j. i \<in> {1 .. dimindex (UNIV:: 'n set)} \<Longrightarrow> j \<in> {1 .. dimindex(UNIV:: 'n set)} \<Longrightarrow> i > j \<Longrightarrow> A$i$j = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
186 |
shows "det A = setprod (\<lambda>i. A$i$i) {1..dimindex(UNIV:: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
187 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
188 |
let ?U = "{1..dimindex(UNIV:: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
189 |
let ?PU = "{p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
190 |
let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) {1 .. dimindex(UNIV :: 'n set)})" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
191 |
have fU: "finite ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
192 |
from finite_permutations[OF fU] have fPU: "finite ?PU" . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
193 |
have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
194 |
{fix p assume p: "p \<in> ?PU -{id}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
195 |
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
196 |
from permutes_natset_ge[OF pU] pid obtain i where |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
197 |
i: "i \<in> ?U" "p i < i" by (metis not_le) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
198 |
from permutes_in_image[OF pU] i(1) have piU: "p i \<in> ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
199 |
from ld[OF i(1) piU i(2)] i(1) have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
200 |
from setprod_zero[OF fU ex] have "?pp p = 0" by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
201 |
then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
202 |
from setsum_superset[OF fPU id0 p0] show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
203 |
unfolding det_def by (simp add: sign_id) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
204 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
205 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
206 |
lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
207 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
208 |
let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
209 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
210 |
let ?f = "\<lambda>i j. ?A$i$j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
211 |
{fix i assume i: "i \<in> ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
212 |
have "?f i i = 1" using i by (vector mat_def)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
213 |
hence th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
214 |
by (auto intro: setprod_cong) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
215 |
{fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i < j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
216 |
have "?f i j = 0" using i j ij by (vector mat_def) } |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
217 |
then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_lowerdiagonal |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
218 |
by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
219 |
also have "\<dots> = 1" unfolding th setprod_1 .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
220 |
finally show ?thesis . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
221 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
222 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
223 |
lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
224 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
225 |
let ?A = "mat 0 :: 'a::comm_ring_1^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
226 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
227 |
let ?f = "\<lambda>i j. ?A$i$j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
228 |
have th:"setprod (\<lambda>i. ?f i i) ?U = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
229 |
apply (rule setprod_zero) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
230 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
231 |
apply (rule bexI[where x=1]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
232 |
using dimindex_ge_1[of "UNIV :: 'n set"] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
233 |
by (simp_all add: mat_def Cart_lambda_beta) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
234 |
{fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i < j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
235 |
have "?f i j = 0" using i j ij by (vector mat_def) } |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
236 |
then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_lowerdiagonal |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
237 |
by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
238 |
also have "\<dots> = 0" unfolding th .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
239 |
finally show ?thesis . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
240 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
241 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
242 |
lemma det_permute_rows: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
243 |
fixes A :: "'a::comm_ring_1^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
244 |
assumes p: "p permutes {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
245 |
shows "det(\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
246 |
apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric] del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
247 |
apply (subst sum_permutations_compose_right[OF p]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
248 |
proof(rule setsum_cong2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
249 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
250 |
let ?PU = "{p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
251 |
let ?Ap = "(\<chi> i. A$p i :: 'a^'n^'n)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
252 |
fix q assume qPU: "q \<in> ?PU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
253 |
have fU: "finite ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
254 |
from qPU have q: "q permutes ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
255 |
from p q have pp: "permutation p" and qp: "permutation q" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
256 |
by (metis fU permutation_permutes)+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
257 |
from permutes_inv[OF p] have ip: "inv p permutes ?U" . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
258 |
{fix i assume i: "i \<in> ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
259 |
from Cart_lambda_beta[rule_format, OF i, of "\<lambda>i. A$ p i"] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
260 |
have "?Ap$i$ (q o p) i = A $ p i $ (q o p) i " by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
261 |
hence "setprod (\<lambda>i. ?Ap$i$ (q o p) i) ?U = setprod (\<lambda>i. A$p i$(q o p) i) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
262 |
by (auto intro: setprod_cong) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
263 |
also have "\<dots> = setprod ((\<lambda>i. A$p i$(q o p) i) o inv p) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
264 |
by (simp only: setprod_permute[OF ip, symmetric]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
265 |
also have "\<dots> = setprod (\<lambda>i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
266 |
by (simp only: o_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
267 |
also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
268 |
finally have thp: "setprod (\<lambda>i. ?Ap$i$ (q o p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
269 |
by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
270 |
show "of_int (sign (q o p)) * setprod (\<lambda>i. ?Ap$i$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A$i$q i) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
271 |
by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
272 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
273 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
274 |
lemma det_permute_columns: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
275 |
fixes A :: "'a::comm_ring_1^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
276 |
assumes p: "p permutes {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
277 |
shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
278 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
279 |
let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
280 |
let ?At = "transp A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
281 |
have "of_int (sign p) * det A = det (transp (\<chi> i. transp A $ p i))" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
282 |
unfolding det_permute_rows[OF p, of ?At] det_transp .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
283 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
284 |
have "?Ap = transp (\<chi> i. transp A $ p i)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
285 |
by (simp add: transp_def Cart_eq Cart_lambda_beta Cart_lambda_beta_perm[OF p]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
286 |
ultimately show ?thesis by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
287 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
288 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
289 |
lemma det_identical_rows: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
290 |
fixes A :: "'a::ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
291 |
assumes i: "i\<in>{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
292 |
and j: "j\<in>{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
293 |
and ij: "i \<noteq> j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
294 |
and r: "row i A = row j A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
295 |
shows "det A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
296 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
297 |
have tha: "\<And>(a::'a) b. a = b ==> b = - a ==> a = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
298 |
by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
299 |
have th1: "of_int (-1) = - 1" by (metis of_int_1 of_int_minus number_of_Min) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
300 |
let ?p = "Fun.swap i j id" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
301 |
let ?A = "\<chi> i. A $ ?p i" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
302 |
from r have "A = ?A" by (simp add: Cart_eq Cart_lambda_beta Cart_lambda_beta_perm[OF permutes_swap_id[OF i j]] row_def swap_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
303 |
hence "det A = det ?A" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
304 |
moreover have "det A = - det ?A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
305 |
by (simp add: det_permute_rows[OF permutes_swap_id[OF i j]] sign_swap_id ij th1) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
306 |
ultimately show "det A = 0" by (metis tha) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
307 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
308 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
309 |
lemma det_identical_columns: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
310 |
fixes A :: "'a::ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
311 |
assumes i: "i\<in>{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
312 |
and j: "j\<in>{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
313 |
and ij: "i \<noteq> j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
314 |
and r: "column i A = column j A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
315 |
shows "det A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
316 |
apply (subst det_transp[symmetric]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
317 |
apply (rule det_identical_rows[OF i j ij]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
318 |
by (metis row_transp i j r) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
319 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
320 |
lemma det_zero_row: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
321 |
fixes A :: "'a::{idom, ring_char_0}^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
322 |
assumes i: "i\<in>{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
323 |
and r: "row i A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
324 |
shows "det A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
325 |
using i r |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
326 |
apply (simp add: row_def det_def Cart_lambda_beta Cart_eq vector_component del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
327 |
apply (rule setsum_0') |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
328 |
apply (clarsimp simp add: sign_nz simp del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
329 |
apply (rule setprod_zero) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
330 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
331 |
apply (rule bexI[where x=i]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
332 |
apply (erule_tac x="a i" in ballE) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
333 |
apply (subgoal_tac "(0\<Colon>'a ^ 'n) $ a i = 0") |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
334 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
335 |
apply (rule zero_index) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
336 |
apply (drule permutes_in_image[of _ _ i]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
337 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
338 |
apply (drule permutes_in_image[of _ _ i]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
339 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
340 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
341 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
342 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
343 |
lemma det_zero_column: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
344 |
fixes A :: "'a::{idom,ring_char_0}^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
345 |
assumes i: "i\<in>{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
346 |
and r: "column i A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
347 |
shows "det A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
348 |
apply (subst det_transp[symmetric]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
349 |
apply (rule det_zero_row[OF i]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
350 |
by (metis row_transp r i) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
351 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
352 |
lemma setsum_lambda_beta[simp]: "setsum (\<lambda>i. ((\<chi> i. g i) :: 'a::{comm_monoid_add}^'n) $ i ) {1 .. dimindex (UNIV :: 'n set)} = setsum g {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
353 |
by (simp add: Cart_lambda_beta) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
354 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
355 |
lemma setprod_lambda_beta[simp]: "setprod (\<lambda>i. ((\<chi> i. g i) :: 'a::{comm_monoid_mult}^'n) $ i ) {1 .. dimindex (UNIV :: 'n set)} = setprod g {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
356 |
apply (rule setprod_cong) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
357 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
358 |
apply (simp add: Cart_lambda_beta') |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
359 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
360 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
361 |
lemma setprod_lambda_beta2[simp]: "setprod (\<lambda>i. ((\<chi> i. g i) :: 'a::{comm_monoid_mult}^'n^'n) $ i$ f i ) {1 .. dimindex (UNIV :: 'n set)} = setprod (\<lambda>i. g i $ f i) {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
362 |
proof(rule setprod_cong[OF refl]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
363 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
364 |
fix i assume i: "i \<in> ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
365 |
from Cart_lambda_beta'[OF i, of g] have |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
366 |
"((\<chi> i. g i) :: 'a^'n^'n) $ i = g i" . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
367 |
hence "((\<chi> i. g i) :: 'a^'n^'n) $ i $ f i = g i $ f i" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
368 |
then |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
369 |
show "((\<chi> i. g i):: 'a^'n^'n) $ i $ f i = g i $ f i" . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
370 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
371 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
372 |
lemma det_row_add: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
373 |
assumes k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
374 |
shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
375 |
det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
376 |
det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
377 |
unfolding det_def setprod_lambda_beta2 setsum_addf[symmetric] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
378 |
proof (rule setsum_cong2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
379 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
380 |
let ?pU = "{p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
381 |
let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::nat \<Rightarrow> 'a::comm_ring_1^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
382 |
let ?g = "(\<lambda> i. if i = k then a i else c i)::nat \<Rightarrow> 'a::comm_ring_1^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
383 |
let ?h = "(\<lambda> i. if i = k then b i else c i)::nat \<Rightarrow> 'a::comm_ring_1^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
384 |
fix p assume p: "p \<in> ?pU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
385 |
let ?Uk = "?U - {k}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
386 |
from p have pU: "p permutes ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
387 |
from k have pkU: "p k \<in> ?U" by (simp only: permutes_in_image[OF pU]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
388 |
note pin[simp] = permutes_in_image[OF pU] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
389 |
have kU: "?U = insert k ?Uk" using k by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
390 |
{fix j assume j: "j \<in> ?Uk" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
391 |
from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
392 |
by simp_all} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
393 |
then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
394 |
and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
395 |
apply - |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
396 |
apply (rule setprod_cong, simp_all)+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
397 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
398 |
have th3: "finite ?Uk" "k \<notin> ?Uk" using k by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
399 |
have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
400 |
unfolding kU[symmetric] .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
401 |
also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
402 |
apply (rule setprod_insert) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
403 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
404 |
using k by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
405 |
also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)" using pkU by (simp add: ring_simps vector_component) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
406 |
also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?h i $ p i) ?Uk)" by (metis th1 th2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
407 |
also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
408 |
unfolding setprod_insert[OF th3] by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
409 |
finally have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?g i $ p i) ?U + setprod (\<lambda>i. ?h i $ p i) ?U" unfolding kU[symmetric] . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
410 |
then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
411 |
by (simp add: ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
412 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
413 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
414 |
lemma det_row_mul: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
415 |
assumes k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
416 |
shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
417 |
c* det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
418 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
419 |
unfolding det_def setprod_lambda_beta2 setsum_right_distrib |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
420 |
proof (rule setsum_cong2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
421 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
422 |
let ?pU = "{p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
423 |
let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::nat \<Rightarrow> 'a::comm_ring_1^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
424 |
let ?g = "(\<lambda> i. if i = k then a i else b i)::nat \<Rightarrow> 'a::comm_ring_1^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
425 |
fix p assume p: "p \<in> ?pU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
426 |
let ?Uk = "?U - {k}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
427 |
from p have pU: "p permutes ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
428 |
from k have pkU: "p k \<in> ?U" by (simp only: permutes_in_image[OF pU]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
429 |
note pin[simp] = permutes_in_image[OF pU] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
430 |
have kU: "?U = insert k ?Uk" using k by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
431 |
{fix j assume j: "j \<in> ?Uk" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
432 |
from j have "?f j $ p j = ?g j $ p j" by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
433 |
then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
434 |
apply - |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
435 |
apply (rule setprod_cong, simp_all) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
436 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
437 |
have th3: "finite ?Uk" "k \<notin> ?Uk" using k by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
438 |
have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
439 |
unfolding kU[symmetric] .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
440 |
also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
441 |
apply (rule setprod_insert) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
442 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
443 |
using k by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
444 |
also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" using pkU by (simp add: ring_simps vector_component) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
445 |
also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
446 |
unfolding th1 using pkU by (simp add: vector_component mult_ac) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
447 |
also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
448 |
unfolding setprod_insert[OF th3] by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
449 |
finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)" unfolding kU[symmetric] . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
450 |
then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
451 |
by (simp add: ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
452 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
453 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
454 |
lemma det_row_0: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
455 |
assumes k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
456 |
shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
457 |
using det_row_mul[OF k, of 0 "\<lambda>i. 1" b] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
458 |
apply (simp) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
459 |
unfolding vector_smult_lzero . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
460 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
461 |
lemma det_row_operation: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
462 |
fixes A :: "'a::ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
463 |
assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
464 |
and j: "j \<in> {1 .. dimindex(UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
465 |
and ij: "i \<noteq> j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
466 |
shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
467 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
468 |
let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
469 |
have th: "row i ?Z = row j ?Z" using i j by (vector row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
470 |
have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
471 |
using i j by (vector row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
472 |
show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
473 |
unfolding det_row_add [OF i] det_row_mul[OF i] det_identical_rows[OF i j ij th] th2 |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
474 |
by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
475 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
476 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
477 |
lemma det_row_span: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
478 |
fixes A :: "'a:: ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
479 |
assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
480 |
and x: "x \<in> span {row j A |j. j\<in> {1 .. dimindex(UNIV :: 'n set)} \<and> j\<noteq> i}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
481 |
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
482 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
483 |
let ?U = "{1 .. dimindex(UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
484 |
let ?S = "{row j A |j. j\<in> ?U \<and> j\<noteq> i}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
485 |
let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
486 |
let ?P = "\<lambda>x. ?d (row i A + x) = det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
487 |
{fix k |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
488 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
489 |
have "(if k = i then row i A + 0 else row k A) = row k A" by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
490 |
then have P0: "?P 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
491 |
apply - |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
492 |
apply (rule cong[of det, OF refl]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
493 |
using i by (vector row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
494 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
495 |
{fix c z y assume zS: "z \<in> ?S" and Py: "?P y" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
496 |
from zS obtain j where j: "z = row j A" "j \<in> ?U" "i \<noteq> j" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
497 |
let ?w = "row i A + y" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
498 |
have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
499 |
have thz: "?d z = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
500 |
apply (rule det_identical_rows[OF i j(2,3)]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
501 |
using i j by (vector row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
502 |
have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
503 |
then have "?P (c*s z + y)" unfolding thz Py det_row_mul[OF i] det_row_add[OF i] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
504 |
by simp } |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
505 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
506 |
ultimately show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
507 |
apply - |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
508 |
apply (rule span_induct_alt[of ?P ?S, OF P0]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
509 |
apply blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
510 |
apply (rule x) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
511 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
512 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
513 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
514 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
515 |
(* May as well do this, though it's a bit unsatisfactory since it ignores *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
516 |
(* exact duplicates by considering the rows/columns as a set. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
517 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
518 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
519 |
lemma det_dependent_rows: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
520 |
fixes A:: "'a::ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
521 |
assumes d: "dependent (rows A)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
522 |
shows "det A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
523 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
524 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
525 |
from d obtain i where i: "i \<in> ?U" "row i A \<in> span (rows A - {row i A})" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
526 |
unfolding dependent_def rows_def by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
527 |
{fix j k assume j: "j \<in>?U" and k: "k \<in> ?U" and jk: "j \<noteq> k" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
528 |
and c: "row j A = row k A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
529 |
from det_identical_rows[OF j k jk c] have ?thesis .} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
530 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
531 |
{assume H: "\<And> i j. i\<in> ?U \<Longrightarrow> j \<in> ?U \<Longrightarrow> i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
532 |
have th0: "- row i A \<in> span {row j A|j. j \<in> ?U \<and> j \<noteq> i}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
533 |
apply (rule span_neg) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
534 |
apply (rule set_rev_mp) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
535 |
apply (rule i(2)) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
536 |
apply (rule span_mono) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
537 |
using H i by (auto simp add: rows_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
538 |
from det_row_span[OF i(1) th0] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
539 |
have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
540 |
unfolding right_minus vector_smult_lzero .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
541 |
with det_row_mul[OF i(1), of "0::'a" "\<lambda>i. 1"] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
542 |
have "det A = 0" by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
543 |
ultimately show ?thesis by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
544 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
545 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
546 |
lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n))" shows "det A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
547 |
by (metis d det_dependent_rows rows_transp det_transp) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
548 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
549 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
550 |
(* Multilinearity and the multiplication formula. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
551 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
552 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
553 |
lemma Cart_lambda_cong: "(\<And>x. x \<in> {1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
554 |
apply (rule iffD1[OF Cart_lambda_unique]) by vector |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
555 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
556 |
lemma det_linear_row_setsum: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
557 |
assumes fS: "finite S" and k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
558 |
shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
559 |
using k |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
560 |
proof(induct rule: finite_induct[OF fS]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
561 |
case 1 thus ?case apply simp unfolding setsum_empty det_row_0[OF k] .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
562 |
next |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
563 |
case (2 x F) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
564 |
then show ?case by (simp add: det_row_add cong del: if_weak_cong) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
565 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
566 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
567 |
lemma finite_bounded_functions: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
568 |
assumes fS: "finite S" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
569 |
shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
570 |
proof(induct k) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
571 |
case 0 |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
572 |
have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
573 |
show ?case by (auto simp add: th) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
574 |
next |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
575 |
case (Suc k) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
576 |
let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
577 |
let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>{1..k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)})" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
578 |
have "?S = {f. (\<forall>i\<in>{1.. Suc k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1.. Suc k} \<longrightarrow> f i = i)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
579 |
apply (auto simp add: image_iff) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
580 |
apply (rule_tac x="x (Suc k)" in bexI) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
581 |
apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
582 |
apply (auto intro: ext) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
583 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
584 |
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
585 |
show ?case by metis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
586 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
587 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
588 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
589 |
lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
590 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
591 |
lemma det_linear_rows_setsum_lemma: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
592 |
assumes fS: "finite S" and k: "k \<le> dimindex (UNIV :: 'n set)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
593 |
shows "det((\<chi> i. if i <= k then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
594 |
setsum (\<lambda>f. det((\<chi> i. if i <= k then a i (f i) else c i)::'a^'n^'n)) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
595 |
{f. (\<forall>i \<in> {1 .. k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
596 |
using k |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
597 |
proof(induct k arbitrary: a c) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
598 |
case 0 |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
599 |
have th0: "\<And>x y. (\<chi> i. if i <= 0 then x i else y i) = (\<chi> i. y i)" by vector |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
600 |
from "0.prems" show ?case unfolding th0 by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
601 |
next |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
602 |
case (Suc k a c) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
603 |
let ?F = "\<lambda>k. {f. (\<forall>i \<in> {1 .. k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
604 |
let ?h = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
605 |
let ?k = "\<lambda>h. (h(Suc k),(\<lambda>i. if i = Suc k then i else h i))" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
606 |
let ?s = "\<lambda> k a c f. det((\<chi> i. if i <= k then a i (f i) else c i)::'a^'n^'n)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
607 |
let ?c = "\<lambda>i. if i = Suc k then a i j else c i" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
608 |
from Suc.prems have Sk: "Suc k \<in> {1 .. dimindex (UNIV :: 'n set)}" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
609 |
from Suc.prems have k': "k \<le> dimindex (UNIV :: 'n set)" by arith |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
610 |
have thif: "\<And>a b c d. (if b \<or> a then c else d) = (if a then c else if b then c else d)" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
611 |
have thif2: "\<And>a b c d e. (if a then b else if c then d else e) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
612 |
(if c then (if a then b else d) else (if a then b else e))" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
613 |
have "det (\<chi> i. if i \<le> Suc k then setsum (a i) S else c i) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
614 |
det (\<chi> i. if i = Suc k then setsum (a i) S |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
615 |
else if i \<le> k then setsum (a i) S else c i)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
616 |
unfolding le_Suc_eq thif .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
617 |
also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<le> k then setsum (a i) S |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
618 |
else if i = Suc k then a i j else c i))" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
619 |
unfolding det_linear_row_setsum[OF fS Sk] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
620 |
apply (subst thif2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
621 |
by (simp cong del: if_weak_cong cong add: if_cong) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
622 |
finally have tha: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
623 |
"det (\<chi> i. if i \<le> Suc k then setsum (a i) S else c i) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
624 |
(\<Sum>(j, f)\<in>S \<times> ?F k. det (\<chi> i. if i \<le> k then a i (f i) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
625 |
else if i = Suc k then a i j |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
626 |
else c i))" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
627 |
unfolding Suc.hyps[OF k'] unfolding setsum_cartesian_product by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
628 |
show ?case unfolding tha |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
629 |
apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"], |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
630 |
blast intro: finite_cartesian_product fS finite_bounded_functions[OF fS], |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
631 |
blast intro: finite_cartesian_product fS finite_bounded_functions[OF fS], auto intro: ext) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
632 |
apply (rule cong[OF refl[of det]]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
633 |
by vector |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
634 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
635 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
636 |
lemma det_linear_rows_setsum: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
637 |
assumes fS: "finite S" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
638 |
shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. (\<forall>i \<in> {1 .. dimindex (UNIV :: 'n set)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1.. dimindex (UNIV :: 'n set)} \<longrightarrow> f i = i)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
639 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
640 |
have th0: "\<And>x y. ((\<chi> i. if i <= dimindex(UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\<chi> i. x i)" by vector |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
641 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
642 |
from det_linear_rows_setsum_lemma[OF fS, of "dimindex (UNIV :: 'n set)" a, unfolded th0, OF order_refl] show ?thesis by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
643 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
644 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
645 |
lemma matrix_mul_setsum_alt: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
646 |
fixes A B :: "'a::comm_ring_1^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
647 |
shows "A ** B = (\<chi> i. setsum (\<lambda>k. A$i$k *s B $ k) {1 .. dimindex (UNIV :: 'n set)})" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
648 |
by (vector matrix_matrix_mult_def setsum_component) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
649 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
650 |
lemma det_rows_mul: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
651 |
"det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
652 |
setprod (\<lambda>i. c i) {1..dimindex(UNIV:: 'n set)} * det((\<chi> i. a i)::'a^'n^'n)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
653 |
proof (simp add: det_def Cart_lambda_beta' setsum_right_distrib vector_component cong add: setprod_cong del: One_nat_def, rule setsum_cong2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
654 |
let ?U = "{1 .. dimindex(UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
655 |
let ?PU = "{p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
656 |
fix p assume pU: "p \<in> ?PU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
657 |
let ?s = "of_int (sign p)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
658 |
from pU have p: "p permutes ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
659 |
have "setprod (\<lambda>i. (c i *s a i) $ p i) ?U = setprod (\<lambda>i. c i * a i $ p i) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
660 |
apply (rule setprod_cong, blast) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
661 |
by (auto simp only: permutes_in_image[OF p] intro: vector_smult_component) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
662 |
also have "\<dots> = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
663 |
unfolding setprod_timesf .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
664 |
finally show "?s * (\<Prod>xa\<in>?U. (c xa *s a xa) $ p xa) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
665 |
setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
666 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
667 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
668 |
lemma det_mul: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
669 |
fixes A B :: "'a::ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
670 |
shows "det (A ** B) = det A * det B" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
671 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
672 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
673 |
let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
674 |
let ?PU = "{p. p permutes ?U}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
675 |
have fU: "finite ?U" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
676 |
have fF: "finite ?F" using finite_bounded_functions[OF fU] . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
677 |
{fix p assume p: "p permutes ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
678 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
679 |
have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
680 |
using p[unfolded permutes_def] by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
681 |
then have PUF: "?PU \<subseteq> ?F" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
682 |
{fix f assume fPU: "f \<in> ?F - ?PU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
683 |
have fUU: "f ` ?U \<subseteq> ?U" using fPU by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
684 |
from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
685 |
"\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" unfolding permutes_def |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
686 |
by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
687 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
688 |
let ?A = "(\<chi> i. A$i$f i *s B$f i) :: 'a^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
689 |
let ?B = "(\<chi> i. B$f i) :: 'a^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
690 |
{assume fni: "\<not> inj_on f ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
691 |
then obtain i j where ij: "i \<in> ?U" "j \<in> ?U" "f i = f j" "i \<noteq> j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
692 |
unfolding inj_on_def by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
693 |
from ij |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
694 |
have rth: "row i ?B = row j ?B" by (vector row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
695 |
from det_identical_rows[OF ij(1,2,4) rth] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
696 |
have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
697 |
unfolding det_rows_mul by simp} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
698 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
699 |
{assume fi: "inj_on f ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
700 |
from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
701 |
unfolding inj_on_def |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
702 |
apply (case_tac "i \<in> ?U") |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
703 |
apply (case_tac "j \<in> ?U") by metis+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
704 |
note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
705 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
706 |
{fix y |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
707 |
from fs f have "\<exists>x. f x = y" by (cases "y \<in> ?U") blast+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
708 |
then obtain x where x: "f x = y" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
709 |
{fix z assume z: "f z = y" from fith x z have "z = x" by metis} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
710 |
with x have "\<exists>!x. f x = y" by blast} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
711 |
with f(3) have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
712 |
ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
713 |
hence zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
714 |
{fix p assume pU: "p \<in> ?PU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
715 |
from pU have p: "p permutes ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
716 |
let ?s = "\<lambda>p. of_int (sign p)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
717 |
let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
718 |
(?s q * (\<Prod>i\<in> ?U. B $ i $ q i))" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
719 |
have "(setsum (\<lambda>q. ?s q * |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
720 |
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
721 |
(setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
722 |
(?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
723 |
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
724 |
proof(rule setsum_cong2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
725 |
fix q assume qU: "q \<in> ?PU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
726 |
hence q: "q permutes ?U" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
727 |
from p q have pp: "permutation p" and pq: "permutation q" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
728 |
unfolding permutation_permutes by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
729 |
have th00: "of_int (sign p) * of_int (sign p) = (1::'a)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
730 |
"\<And>a. of_int (sign p) * (of_int (sign p) * a) = a" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
731 |
unfolding mult_assoc[symmetric] unfolding of_int_mult[symmetric] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
732 |
by (simp_all add: sign_idempotent) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
733 |
have ths: "?s q = ?s p * ?s (q o inv p)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
734 |
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
735 |
by (simp add: th00 mult_ac sign_idempotent sign_compose) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
736 |
have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) o p) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
737 |
by (rule setprod_permute[OF p]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
738 |
have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = setprod (\<lambda>i. A$i$p i) ?U * setprod (\<lambda>i. B$i$ q (inv p i)) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
739 |
unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
740 |
apply (rule setprod_cong[OF refl]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
741 |
using permutes_in_image[OF q] by vector |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
742 |
show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\<lambda>i. B$i$(q o inv p) i) ?U)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
743 |
using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
744 |
by (simp add: sign_nz th00 ring_simps sign_idempotent sign_compose) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
745 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
746 |
} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
747 |
then have th2: "setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
748 |
unfolding det_def setsum_product |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
749 |
by (rule setsum_cong2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
750 |
have "det (A**B) = setsum (\<lambda>f. det (\<chi> i. A $ i $ f i *s B $ f i)) ?F" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
751 |
unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
752 |
also have "\<dots> = setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
753 |
unfolding setsum_superset[OF fF PUF zth, symmetric] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
754 |
unfolding det_rows_mul .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
755 |
finally show ?thesis unfolding th2 . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
756 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
757 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
758 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
759 |
(* Relation to invertibility. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
760 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
761 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
762 |
lemma invertible_left_inverse: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
763 |
fixes A :: "real^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
764 |
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
765 |
by (metis invertible_def matrix_left_right_inverse) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
766 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
767 |
lemma invertible_righ_inverse: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
768 |
fixes A :: "real^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
769 |
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
770 |
by (metis invertible_def matrix_left_right_inverse) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
771 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
772 |
lemma invertible_det_nz: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
773 |
fixes A::"real ^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
774 |
shows "invertible A \<longleftrightarrow> det A \<noteq> 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
775 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
776 |
{assume "invertible A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
777 |
then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
778 |
unfolding invertible_righ_inverse by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
779 |
hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
780 |
hence "det A \<noteq> 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
781 |
apply (simp add: det_mul det_I) by algebra } |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
782 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
783 |
{assume H: "\<not> invertible A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
784 |
let ?U = "{1 .. dimindex(UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
785 |
have fU: "finite ?U" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
786 |
from H obtain c i where c: "setsum (\<lambda>i. c i *s row i A) ?U = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
787 |
and iU: "i \<in> ?U" and ci: "c i \<noteq> 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
788 |
unfolding invertible_righ_inverse |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
789 |
unfolding matrix_right_invertible_independent_rows by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
790 |
have stupid: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
791 |
apply (drule_tac f="op + (- a)" in cong[OF refl]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
792 |
apply (simp only: ab_left_minus add_assoc[symmetric]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
793 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
794 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
795 |
from c ci |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
796 |
have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s c j *s row j A) (?U - {i})" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
797 |
unfolding setsum_diff1'[OF fU iU] setsum_cmul |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
798 |
apply (simp add: field_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
799 |
apply (rule vector_mul_lcancel_imp[OF ci]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
800 |
apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
801 |
unfolding stupid .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
802 |
have thr: "- row i A \<in> span {row j A| j. j\<in> ?U \<and> j \<noteq> i}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
803 |
unfolding thr0 |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
804 |
apply (rule span_setsum) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
805 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
806 |
apply (rule ballI) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
807 |
apply (rule span_mul)+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
808 |
apply (rule span_superset) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
809 |
apply auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
810 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
811 |
let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
812 |
have thrb: "row i ?B = 0" using iU by (vector row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
813 |
have "det A = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
814 |
unfolding det_row_span[OF iU thr, symmetric] right_minus |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
815 |
unfolding det_zero_row[OF iU thrb] ..} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
816 |
ultimately show ?thesis by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
817 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
818 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
819 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
820 |
(* Cramer's rule. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
821 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
822 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
823 |
lemma cramer_lemma_transp: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
824 |
fixes A:: "'a::ordered_idom^'n^'n" and x :: "'a ^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
825 |
assumes k: "k \<in> {1 .. dimindex(UNIV ::'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
826 |
shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) {1 .. dimindex(UNIV::'n set)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
827 |
else row i A)::'a^'n^'n) = x$k * det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
828 |
(is "?lhs = ?rhs") |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
829 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
830 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
831 |
let ?Uk = "?U - {k}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
832 |
have U: "?U = insert k ?Uk" using k by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
833 |
have fUk: "finite ?Uk" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
834 |
have kUk: "k \<notin> ?Uk" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
835 |
have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
836 |
by (vector ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
837 |
have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
838 |
have "(\<chi> i. row i A) = A" by (vector row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
839 |
then have thd1: "det (\<chi> i. row i A) = det A" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
840 |
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" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
841 |
apply (rule det_row_span[OF k]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
842 |
apply (rule span_setsum[OF fUk]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
843 |
apply (rule ballI) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
844 |
apply (rule span_mul) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
845 |
apply (rule span_superset) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
846 |
apply auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
847 |
done |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
848 |
show "?lhs = x$k * det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
849 |
apply (subst U) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
850 |
unfolding setsum_insert[OF fUk kUk] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
851 |
apply (subst th00) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
852 |
unfolding add_assoc |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
853 |
apply (subst det_row_add[OF k]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
854 |
unfolding thd0 |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
855 |
unfolding det_row_mul[OF k] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
856 |
unfolding th001[of k "\<lambda>i. row i A"] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
857 |
unfolding thd1 by (simp add: ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
858 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
859 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
860 |
lemma cramer_lemma: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
861 |
fixes A :: "'a::ordered_idom ^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
862 |
assumes k: "k \<in> {1 .. dimindex (UNIV :: 'n set)}" (is " _ \<in> ?U") |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
863 |
shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
864 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
865 |
have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transp A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
866 |
by (auto simp add: row_transp intro: setsum_cong2) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
867 |
show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
868 |
unfolding matrix_mult_vsum |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
869 |
unfolding cramer_lemma_transp[OF k, of x "transp A", unfolded det_transp, symmetric] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
870 |
unfolding stupid[of "\<lambda>i. x$i"] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
871 |
apply (subst det_transp[symmetric]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
872 |
apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
873 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
874 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
875 |
lemma cramer: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
876 |
fixes A ::"real^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
877 |
assumes d0: "det A \<noteq> 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
878 |
shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
879 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
880 |
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
881 |
unfolding invertible_det_nz[symmetric] invertible_def by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
882 |
have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
883 |
hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
884 |
then have xe: "\<exists>x. A*v x = b" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
885 |
{fix x assume x: "A *v x = b" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
886 |
have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
887 |
unfolding x[symmetric] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
888 |
using d0 by (simp add: Cart_eq Cart_lambda_beta' cramer_lemma field_simps)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
889 |
with xe show ?thesis by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
890 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
891 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
892 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
893 |
(* Orthogonality of a transformation and matrix. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
894 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
895 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
896 |
definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
897 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
898 |
lemma orthogonal_transformation: "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^'n). norm (f v) = norm v)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
899 |
unfolding orthogonal_transformation_def |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
900 |
apply auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
901 |
apply (erule_tac x=v in allE)+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
902 |
apply (simp add: real_vector_norm_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
903 |
by (simp add: dot_norm linear_add[symmetric]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
904 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
905 |
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
906 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
907 |
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
908 |
by (metis matrix_left_right_inverse orthogonal_matrix_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
909 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
910 |
lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
911 |
by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
912 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
913 |
lemma orthogonal_matrix_mul: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
914 |
fixes A :: "real ^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
915 |
assumes oA : "orthogonal_matrix A" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
916 |
and oB: "orthogonal_matrix B" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
917 |
shows "orthogonal_matrix(A ** B)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
918 |
using oA oB |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
919 |
unfolding orthogonal_matrix matrix_transp_mul |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
920 |
apply (subst matrix_mul_assoc) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
921 |
apply (subst matrix_mul_assoc[symmetric]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
922 |
by (simp add: matrix_mul_rid) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
923 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
924 |
lemma orthogonal_transformation_matrix: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
925 |
fixes f:: "real^'n \<Rightarrow> real^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
926 |
shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
927 |
(is "?lhs \<longleftrightarrow> ?rhs") |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
928 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
929 |
let ?mf = "matrix f" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
930 |
let ?ot = "orthogonal_transformation f" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
931 |
let ?U = "{1 .. dimindex (UNIV :: 'n set)}" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
932 |
have fU: "finite ?U" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
933 |
let ?m1 = "mat 1 :: real ^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
934 |
{assume ot: ?ot |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
935 |
from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
936 |
unfolding orthogonal_transformation_def orthogonal_matrix by blast+ |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
937 |
{fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
938 |
let ?A = "transp ?mf ** ?mf" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
939 |
have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
940 |
"\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
941 |
by simp_all |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
942 |
from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] i j |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
943 |
have "?A$i$j = ?m1 $ i $ j" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
944 |
by (simp add: Cart_lambda_beta' dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def del: One_nat_def)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
945 |
hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
946 |
with lf have ?rhs by blast} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
947 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
948 |
{assume lf: "linear f" and om: "orthogonal_matrix ?mf" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
949 |
from lf om have ?lhs |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
950 |
unfolding orthogonal_matrix_def norm_eq orthogonal_transformation |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
951 |
unfolding matrix_works[OF lf, symmetric] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
952 |
apply (subst dot_matrix_vector_mul) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
953 |
by (simp add: dot_matrix_product matrix_mul_lid del: One_nat_def)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
954 |
ultimately show ?thesis by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
955 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
956 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
957 |
lemma det_orthogonal_matrix: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
958 |
fixes Q:: "'a::ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
959 |
assumes oQ: "orthogonal_matrix Q" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
960 |
shows "det Q = 1 \<or> det Q = - 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
961 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
962 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
963 |
have th: "\<And>x::'a. x = 1 \<or> x = - 1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x") |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
964 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
965 |
fix x:: 'a |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
966 |
have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
967 |
have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
968 |
apply (subst eq_iff_diff_eq_0) by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
969 |
have "x*x = 1 \<longleftrightarrow> x*x - 1 = 0" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
970 |
also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1" unfolding th0 th1 by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
971 |
finally show "?ths x" .. |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
972 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
973 |
from oQ have "Q ** transp Q = mat 1" by (metis orthogonal_matrix_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
974 |
hence "det (Q ** transp Q) = det (mat 1:: 'a^'n^'n)" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
975 |
hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transp) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
976 |
then show ?thesis unfolding th . |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
977 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
978 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
979 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
980 |
(* Linearity of scaling, and hence isometry, that preserves origin. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
981 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
982 |
lemma scaling_linear: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
983 |
fixes f :: "real ^'n \<Rightarrow> real ^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
984 |
assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
985 |
shows "linear f" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
986 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
987 |
{fix v w |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
988 |
{fix x note fd[rule_format, of x 0, unfolded dist_def f0 diff_0_right] } |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
989 |
note th0 = this |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
990 |
have "f v \<bullet> f w = c^2 * (v \<bullet> w)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
991 |
unfolding dot_norm_neg dist_def[symmetric] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
992 |
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
993 |
note fc = this |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
994 |
show ?thesis unfolding linear_def vector_eq |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
995 |
by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
996 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
997 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
998 |
lemma isometry_linear: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
999 |
"f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1000 |
\<Longrightarrow> linear f" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1001 |
by (rule scaling_linear[where c=1]) simp_all |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1002 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1003 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1004 |
(* Hence another formulation of orthogonal transformation. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1005 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1006 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1007 |
lemma orthogonal_transformation_isometry: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1008 |
"orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1009 |
unfolding orthogonal_transformation |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1010 |
apply (rule iffI) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1011 |
apply clarify |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1012 |
apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1013 |
apply (rule conjI) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1014 |
apply (rule isometry_linear) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1015 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1016 |
apply simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1017 |
apply clarify |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1018 |
apply (erule_tac x=v in allE) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1019 |
apply (erule_tac x=0 in allE) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1020 |
by (simp add: dist_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1021 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1022 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1023 |
(* Can extend an isometry from unit sphere. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1024 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1025 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1026 |
lemma isometry_sphere_extend: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1027 |
fixes f:: "real ^'n \<Rightarrow> real ^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1028 |
assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1029 |
and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1030 |
shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1031 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1032 |
{fix x y x' y' x0 y0 x0' y0' :: "real ^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1033 |
assume H: "x = norm x *s x0" "y = norm y *s y0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1034 |
"x' = norm x *s x0'" "y' = norm y *s y0'" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1035 |
"norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1036 |
"norm(x0' - y0') = norm(x0 - y0)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1037 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1038 |
have "norm(x' - y') = norm(x - y)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1039 |
apply (subst H(1)) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1040 |
apply (subst H(2)) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1041 |
apply (subst H(3)) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1042 |
apply (subst H(4)) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1043 |
using H(5-9) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1044 |
apply (simp add: norm_eq norm_eq_1) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1045 |
apply (simp add: dot_lsub dot_rsub dot_lmult dot_rmult) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1046 |
apply (simp add: ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1047 |
by (simp only: right_distrib[symmetric])} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1048 |
note th0 = this |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1049 |
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1050 |
{fix x:: "real ^'n" assume nx: "norm x = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1051 |
have "?g x = f x" using nx by (simp add: norm_eq_0[symmetric])} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1052 |
hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1053 |
have g0: "?g 0 = 0" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1054 |
{fix x y :: "real ^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1055 |
{assume "x = 0" "y = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1056 |
then have "dist (?g x) (?g y) = dist x y" by simp } |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1057 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1058 |
{assume "x = 0" "y \<noteq> 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1059 |
then have "dist (?g x) (?g y) = dist x y" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1060 |
apply (simp add: dist_def norm_neg norm_mul norm_eq_0) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1061 |
apply (rule f1[rule_format]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1062 |
by(simp add: norm_mul norm_eq_0 field_simps)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1063 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1064 |
{assume "x \<noteq> 0" "y = 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1065 |
then have "dist (?g x) (?g y) = dist x y" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1066 |
apply (simp add: dist_def norm_neg norm_mul norm_eq_0) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1067 |
apply (rule f1[rule_format]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1068 |
by(simp add: norm_mul norm_eq_0 field_simps)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1069 |
moreover |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1070 |
{assume z: "x \<noteq> 0" "y \<noteq> 0" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1071 |
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)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1072 |
"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1073 |
"norm (inverse (norm x) *s x) = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1074 |
"norm (f (inverse (norm x) *s x)) = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1075 |
"norm (inverse (norm y) *s y) = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1076 |
"norm (f (inverse (norm y) *s y)) = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1077 |
"norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1078 |
norm (inverse (norm x) *s x - inverse (norm y) *s y)" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1079 |
using z |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1080 |
by (auto simp add: norm_eq_0 vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1081 |
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1082 |
by (simp add: dist_def)} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1083 |
ultimately have "dist (?g x) (?g y) = dist x y" by blast} |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1084 |
note thd = this |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1085 |
show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1086 |
apply (rule exI[where x= ?g]) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1087 |
unfolding orthogonal_transformation_isometry |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1088 |
using g0 thfg thd by metis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1089 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1090 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1091 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1092 |
(* Rotation, reflection, rotoinversion. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1093 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1094 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1095 |
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1096 |
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1097 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1098 |
lemma orthogonal_rotation_or_rotoinversion: |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1099 |
fixes Q :: "'a::ordered_idom^'n^'n" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1100 |
shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1101 |
by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1102 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1103 |
(* Explicit formulas for low dimensions. *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1104 |
(* ------------------------------------------------------------------------- *) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1105 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1106 |
lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1107 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1108 |
lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1109 |
by (simp add: nat_number setprod_numseg mult_commute) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1110 |
lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1111 |
by (simp add: nat_number setprod_numseg mult_commute) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1112 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1113 |
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1114 |
by (simp add: det_def dimindex_def permutes_sing sign_id del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1115 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1116 |
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1117 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1118 |
have f12: "finite {2::nat}" "1 \<notin> {2::nat}" by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1119 |
have th12: "{1 .. 2} = insert (1::nat) {2}" by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1120 |
show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1121 |
apply (simp add: det_def dimindex_def th12 del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1122 |
unfolding setsum_over_permutations_insert[OF f12] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1123 |
unfolding permutes_sing |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1124 |
apply (simp add: sign_swap_id sign_id swap_id_eq del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1125 |
by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31)) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1126 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1127 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1128 |
lemma det_3: "det (A::'a::comm_ring_1^3^3) = |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1129 |
A$1$1 * A$2$2 * A$3$3 + |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1130 |
A$1$2 * A$2$3 * A$3$1 + |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1131 |
A$1$3 * A$2$1 * A$3$2 - |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1132 |
A$1$1 * A$2$3 * A$3$2 - |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1133 |
A$1$2 * A$2$1 * A$3$3 - |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1134 |
A$1$3 * A$2$2 * A$3$1" |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1135 |
proof- |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1136 |
have f123: "finite {(2::nat), 3}" "1 \<notin> {(2::nat), 3}" by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1137 |
have f23: "finite {(3::nat)}" "2 \<notin> {(3::nat)}" by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1138 |
have th12: "{1 .. 3} = insert (1::nat) (insert 2 {3})" by auto |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1139 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1140 |
show ?thesis |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1141 |
apply (simp add: det_def dimindex_def th12 del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1142 |
unfolding setsum_over_permutations_insert[OF f123] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1143 |
unfolding setsum_over_permutations_insert[OF f23] |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1144 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1145 |
unfolding permutes_sing |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1146 |
apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq del: One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1147 |
apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31) One_nat_def) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1148 |
by (simp add: ring_simps) |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1149 |
qed |
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1150 |
|
57dccccc37b3
Traces, Determinant of square matrices and some properties
chaieb
parents:
diff
changeset
|
1151 |
end |