(* Author: René Thiemann Akihisa Yamada License: BSD *) section ‹Determinants› text ‹Most of the following definitions and proofs on determinants have been copied and adapted from ~~/src/HOL/Multivariate-Analysis/Determinants.thy. Exceptions are \emph{det-identical-rows}. We further generalized some lemmas, e.g., that the determinant is 0 iff the kernel of a matrix is non-empty is available for integral domains, not just for fields.› theory Determinant imports Missing_Misc Column_Operations "HOL-Computational_Algebra.Polynomial_Factorial" (* Only for to_fract. Probably not the right place. *) Polynomial_Interpolation.Ring_Hom Polynomial_Interpolation.Missing_Unsorted begin definition det:: "'a mat ⇒ 'a :: comm_ring_1" where "det A = (if dim_row A = dim_col A then (∑ p ∈ {p. p permutes {0 ..< dim_row A}}. signof p * (∏ i = 0 ..< dim_row A. A $$ (i, p i))) else 0)" lemma(in ring_hom) hom_signof[simp]: "hom (signof p) = signof p" by (simp add: hom_uminus sign_def) lemma(in comm_ring_hom) hom_det[simp]: "det (map_mat hom A) = hom (det A)" unfolding det_def by (auto simp: hom_distribs) lemma det_def': "A ∈ carrier_mat n n ⟹ det A = (∑ p ∈ {p. p permutes {0 ..< n}}. signof p * (∏ i = 0 ..< n. A $$ (i, p i)))" unfolding det_def by auto lemma det_smult[simp]: "det (a ⋅⇩_{m}A) = a ^ dim_col A * det A" proof - have [simp]: "(∏i = 0..<dim_col A. a) = a ^ dim_col A" by(subst prod_constant;simp) show ?thesis unfolding det_def unfolding index_smult_mat by (auto intro: sum.cong simp: sum_distrib_left prod.distrib) qed lemma det_transpose: assumes A: "A ∈ carrier_mat n n" shows "det (transpose_mat A) = det A" proof - let ?di = "λA i j. A $$ (i,j)" let ?U = "{0 ..< n}" have fU: "finite ?U" by simp let ?inv = "Hilbert_Choice.inv" { fix p assume p: "p ∈ {p. p permutes ?U}" from p have pU: "p permutes ?U" by blast have sth: "signof (?inv p) = signof p" by (rule signof_inv[OF _ pU], simp) from permutes_inj[OF pU] have pi: "inj_on p ?U" by (blast intro: subset_inj_on) let ?f = "λi. transpose_mat A $$ (i, ?inv p i)" note pU_U = permutes_image[OF pU] note [simp] = permutes_less[OF pU] have "prod ?f ?U = prod ?f (p ` ?U)" using pU_U by simp also have "… = prod (?f ∘ p) ?U" by (rule prod.reindex[OF pi]) also have "… = prod (λi. A $$ (i, p i)) ?U" by (rule prod.cong, insert A, auto) finally have "signof (?inv p) * prod ?f ?U = signof p * prod (λi. A $$ (i, p i)) ?U" unfolding sth by simp } then show ?thesis unfolding det_def using A by (simp, subst sum_permutations_inverse, intro sum.cong, auto) qed lemma det_col: assumes A: "A ∈ carrier_mat n n" shows "det A = (∑ p | p permutes {0 ..< n}. signof p * (∏j<n. A $$ (p j, j)))" (is "_ = (sum (λp. _ * ?prod p) ?P)") proof - let ?i = "Hilbert_Choice.inv" let ?N = "{0 ..< n}" let ?f = "λp. signof p * ?prod p" let ?prod' = "λp. ∏j<n. A $$ (j, ?i p j)" let ?prod'' = "λp. ∏j<n. A $$ (j, p j)" let ?f' = "λp. signof (?i p) * ?prod' p" let ?f'' = "λp. signof p * ?prod'' p" let ?P' = "{ ?i p | p. p permutes ?N }" have [simp]: "{0..<n} = {..<n}" by auto have "sum ?f ?P = sum ?f' ?P" proof (rule sum.cong[OF refl],unfold mem_Collect_eq) fix p assume p: "p permutes ?N" have [simp]: "?prod p = ?prod' p" using permutes_prod[OF p, of "λx y. A $$ (x,y)"] by auto have [simp]: "signof p = signof (?i p)" apply(rule signof_inv[symmetric]) using p by auto show "?f p = ?f' p" by auto qed also have "... = sum ?f' ?P'" by (rule sum.cong[OF image_inverse_permutations[symmetric]],auto) also have "... = sum ?f'' ?P" unfolding sum.reindex[OF inv_inj_on_permutes,unfolded image_Collect] unfolding o_def apply (rule sum.cong[OF refl]) using inv_inv_eq[OF permutes_bij] by force finally show ?thesis unfolding det_def'[OF A] by auto qed lemma mat_det_left_def: assumes A: "A ∈ carrier_mat n n" shows "det A = (∑p∈{p. p permutes {0..<dim_row A}}. signof p * (∏i = 0 ..< dim_row A. A $$ (p i, i)))" proof - have cong: "⋀ a b c. b = c ⟹ a * b = a * c" by simp show ?thesis unfolding det_transpose[OF A, symmetric] unfolding det_def index_transpose_mat using A by simp qed lemma det_upper_triangular: assumes ut: "upper_triangular A" and m: "A ∈ carrier_mat n n" shows "det A = prod_list (diag_mat A)" proof - note det_def = det_def'[OF m] let ?U = "{0..<n}" let ?PU = "{p. p permutes ?U}" let ?pp = "λp. signof p * (∏ i = 0 ..< n. A $$ (i, p i))" have fU: "finite ?U" by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . have id0: "{id} ⊆ ?PU" by (auto simp add: permutes_id) { fix p assume p: "p ∈ ?PU - {id}" from p have pU: "p permutes ?U" and pid: "p ≠ id" by blast+ from permutes_natset_ge[OF pU] pid obtain i where i: "p i < i" and "i < n" by fastforce from upper_triangularD[OF ut i] ‹i < n› m have ex:"∃i ∈ ?U. A $$ (i,p i) = 0" by auto have "(∏ i = 0 ..< n. A $$ (i, p i)) = 0" by (rule prod_zero[OF fU ex]) hence "?pp p = 0" by simp } then have p0: "⋀ p. p ∈ ?PU - {id} ⟹ ?pp p = 0" by blast from m have dim: "dim_row A = n" by simp have "det A = (∑ p ∈ ?PU. ?pp p)" unfolding det_def by auto also have "… = ?pp id + (∑ p ∈ ?PU - {id}. ?pp p)" by (rule sum.remove, insert id0 fPU m, auto simp: p0) also have "(∑ p ∈ ?PU - {id}. ?pp p) = 0" by (rule sum.neutral, insert fPU, auto simp: p0) finally show ?thesis using m by (auto simp: prod_list_diag_prod) qed lemma det_single: assumes "A ∈ carrier_mat 1 1" shows "det A = A $$ (0,0)" by (subst det_upper_triangular[of _ 1], insert assms, auto simp: diag_mat_def) lemma det_one[simp]: "det (1⇩_{m}n) = 1" proof - have "det (1⇩_{m}n) = prod_list (diag_mat (1⇩_{m}n))" by (rule det_upper_triangular[of _ n], auto) also have "… = 1" by (induct n, auto) finally show ?thesis . qed lemma det_zero[simp]: assumes "n > 0" shows "det (0⇩_{m}n n) = 0" proof - have "det (0⇩_{m}n n) = prod_list (diag_mat (0⇩_{m}n n))" by (rule det_upper_triangular[of _ n], auto) also have "… = 0" using ‹n > 0› by (cases n, auto) finally show ?thesis . qed lemma det_dim_zero[simp]: "A ∈ carrier_mat 0 0 ⟹ det A = 1" unfolding det_def carrier_mat_def sign_def by auto lemma det_lower_triangular: assumes ld: "⋀i j. i < j ⟹ j < n ⟹ A $$ (i,j) = 0" and m: "A ∈ carrier_mat n n" shows "det A = prod_list (diag_mat A)" proof - have "det A = det (transpose_mat A)" using det_transpose[OF m] by simp also have "… = prod_list (diag_mat (transpose_mat A))" by (rule det_upper_triangular, insert m ld, auto) finally show ?thesis using m by simp qed lemma det_permute_rows: assumes A: "A ∈ carrier_mat n n" and p: "p permutes {0 ..< (n :: nat)}" shows "det (mat n n (λ (i,j). A $$ (p i, j))) = signof p * det A" proof - let ?U = "{0 ..< (n :: nat)}" have cong: "⋀ a b c. b = c ⟹ a * b = a * c" by auto have "det (mat n n (λ (i,j). A $$ (p i, j))) = (∑ q ∈ {q . q permutes ?U}. signof q * (∏ i ∈ ?U. A $$ (p i, q i)))" unfolding det_def using A p by auto also have "… = (∑ q ∈ {q . q permutes ?U}. signof (q ∘ p) * (∏ i ∈ ?U. A $$ (p i, (q ∘ p) i)))" by (rule sum_permutations_compose_right[OF p]) finally have 1: "det (mat n n (λ (i,j). A $$ (p i, j))) = (∑ q ∈ {q . q permutes ?U}. signof (q ∘ p) * (∏ i ∈ ?U. A $$ (p i, (q ∘ p) i)))" . have 2: "signof p * det A = (∑ q∈{q. q permutes ?U}. signof p * signof q * (∏i∈ ?U. A $$ (i, q i)))" unfolding det_def'[OF A] sum_distrib_left by (simp add: ac_simps) show ?thesis unfolding 1 2 proof (rule sum.cong, insert p A, auto) fix q assume q: "q permutes ?U" let ?inv = "Hilbert_Choice.inv" from permutes_inv[OF p] have ip: "?inv p permutes ?U" . have "prod (λi. A $$ (p i, (q ∘ p) i)) ?U = prod (λi. A $$ ((p ∘ ?inv p) i, (q ∘ (p ∘ ?inv p)) i)) ?U" unfolding o_def by (rule trans[OF prod.permute[OF ip] prod.cong], insert A p q, auto) also have "… = prod (λi. A$$(i,q i)) ?U" by (simp only: o_def permutes_inverses[OF p]) finally have thp: "prod (λi. A $$ (p i, (q ∘ p) i)) ?U = prod (λi. A$$(i,q i)) ?U" . show "signof (q ∘ p) * (∏i∈{0..<n}. A $$ (p i, q (p i))) = signof p * signof q * (∏i∈{0..<n}. A $$ (i, q i))" unfolding thp[symmetric] signof_compose[OF q p] by (simp add: ac_simps) qed qed lemma det_multrow_mat: assumes k: "k < n" shows "det (multrow_mat n k a) = a" proof (rule trans[OF det_lower_triangular[of n]], unfold prod_list_diag_prod) let ?f = "λ i. multrow_mat n k a $$ (i, i)" have "(∏i∈{0..<n}. ?f i) = ?f k * (∏i∈{0..<n} - {k}. ?f i)" by (rule prod.remove, insert k, auto) also have "(∏i∈{0..<n} - {k}. ?f i) = 1" by (rule prod.neutral, auto) finally show "(∏i∈{0..<dim_row (multrow_mat n k a)}. ?f i) = a" using k by simp qed (insert k, auto) lemma swap_rows_mat_eq_permute: "k < n ⟹ l < n ⟹ swaprows_mat n k l = mat n n (λ(i, j). 1⇩_{m}n $$ (transpose k l i, j))" by (rule eq_matI) (auto simp add: transpose_def) lemma det_swaprows_mat: assumes k: "k < n" and l: "l < n" and kl: "k ≠ l" shows "det (swaprows_mat n k l) = - 1" proof - let ?n = "{0 ..< (n :: nat)}" let ?p = "transpose k l" have p: "?p permutes ?n" by (rule permutes_swap_id, insert k l, auto) show ?thesis by (rule trans[OF trans[OF _ det_permute_rows[OF one_carrier_mat[of n] p]]], subst swap_rows_mat_eq_permute[OF k l], auto simp: sign_swap_id kl) qed lemma det_addrow_mat: assumes l: "k ≠ l" shows "det (addrow_mat n a k l) = 1" proof - have "det (addrow_mat n a k l) = prod_list (diag_mat (addrow_mat n a k l))" proof (cases "k < l") case True show ?thesis by (rule det_upper_triangular[of _ n], insert True, auto intro!: upper_triangularI) next case False show ?thesis by (rule det_lower_triangular[of n], insert False, auto) qed also have "… = 1" unfolding prod_list_diag_prod by (rule prod.neutral, insert l, auto) finally show ?thesis . qed text ‹The following proof is new, as it does not use $2 \neq 0$ as in Multivariate-Analysis.› lemma det_identical_rows: assumes A: "A ∈ carrier_mat n n" and ij: "i ≠ j" and i: "i < n" and j: "j < n" and r: "row A i = row A j" shows "det A = 0" proof- let ?p = "transpose i j" let ?n = "{0 ..< n}" have sp: "signof ?p = - 1" "sign ?p = (- 1 :: int)" using ij by (auto simp add: sign_swap_id) let ?f = "λ p. signof p * (∏i∈?n. A $$ (p i, i))" let ?all = "{p. p permutes ?n}" let ?one = "{p. p permutes ?n ∧ sign p = (1 :: int)}" let ?none = "{p. p permutes ?n ∧ sign p ≠ (1 :: int)}" let ?pone = "(λ p. ?p o p) ` ?one" have split: "?one ∪ ?none = ?all" by auto have p: "?p permutes ?n" by (rule permutes_swap_id, insert i j, auto) from permutes_inj[OF p] have injp: "inj ?p" by auto { fix q assume q: "q permutes ?n" have "(∏k∈?n. A $$ (?p (q k), k)) = (∏k∈?n. A $$ (q k, k))" proof (rule prod.cong) fix k assume k: "k ∈ ?n" from r have row: "row A i $ k = row A j $ k" by simp hence "A $$ (i,k) = A $$ (j,k)" using k i j A by auto thus "A $$ (?p (q k), k) = A $$ (q k, k)" by (cases "q k = i", auto, cases "q k = j", auto) qed (insert A q, auto) } note * = this have pp: "⋀ q. q permutes ?n ⟹ permutation q" unfolding permutation_permutes by auto have "det A = (∑p∈ ?one ∪ ?none. ?f p)" using A unfolding mat_det_left_def[OF A] split by simp also have "… = (∑p∈ ?one. ?f p) + (∑p∈ ?none. ?f p)" by (rule sum.union_disjoint, insert A, auto simp: finite_permutations) also have "?none = ?pone" proof - { fix q assume "q ∈ ?none" hence q: "q permutes ?n" and sq: "sign q = (- 1 :: int)" unfolding sign_def by auto from permutes_compose[OF q p] sign_compose[OF pp[OF p] pp[OF q], unfolded sp sq] have "?p o q ∈ ?one" by auto hence "?p o (?p o q) ∈ ?pone" by auto also have "?p o (?p o q) = q" by (auto simp: swap_id_eq) finally have "q ∈ ?pone" . } moreover { fix pq assume "pq ∈ ?pone" then obtain q where q: "q ∈ ?one" and pq: "pq = ?p o q" by auto from q have q: "q permutes ?n" and sq: "sign q = (1 :: int)" by auto from sign_compose[OF pp[OF p] pp[OF q], unfolded sq sp] have spq: "sign pq = (- 1 :: int)" unfolding pq by auto from permutes_compose[OF q p] have pq: "pq permutes ?n" unfolding pq by auto from pq spq have "pq ∈ ?none" by auto } ultimately show ?thesis by blast qed also have "(∑p∈ ?pone. ?f p) = (∑p∈ ?one. ?f (?p o p))" proof (rule trans[OF sum.reindex]) show "inj_on ((∘) ?p) ?one" using fun.inj_map[OF injp] unfolding inj_on_def by auto qed simp also have "(∑p∈ ?one. ?f p) + (∑p∈ ?one. ?f (?p o p)) = (∑p∈ ?one. ?f p + ?f (?p o p))" by (rule sum.distrib[symmetric]) also have "… = 0" by (rule sum.neutral, insert A, auto simp: sp sign_compose[OF pp[OF p] pp] ij finite_permutations *) finally show ?thesis . qed lemma det_row_0: assumes k: "k < n" and c: "c ∈ {0 ..< n} → carrier_vec n" shows "det (mat⇩_{r}n n (λi. if i = k then 0⇩_{v}n else c i)) = 0" proof - { fix p assume p: "p permutes {0 ..< n}" have "(∏i∈{0..<n}. mat⇩_{r}n n (λi. if i = k then 0⇩_{v}n else c i) $$ (i, p i)) = 0" by (rule prod_zero[OF _ bexI[of _ k]], insert k p c[unfolded carrier_vec_def], auto) } thus ?thesis unfolding det_def by simp qed lemma det_row_add: assumes abc: "a k ∈ carrier_vec n" "b k ∈ carrier_vec n" "c ∈ {0..<n} → carrier_vec n" and k: "k < n" shows "det(mat⇩_{r}n n (λ i. if i = k then a i + b i else c i)) = det(mat⇩_{r}n n (λ i. if i = k then a i else c i)) + det(mat⇩_{r}n n (λ i. if i = k then b i else c i))" (is "?lhs = ?rhs") proof - let ?n = "{0..<n}" let ?m = "λ a b p i. mat⇩_{r}n n (λi. if i = k then a i else b i) $$ (i, p i)" let ?c = "λ p i. mat⇩_{r}n n c $$ (i, p i)" let ?ab = "λ i. a i + b i" note intros = add_carrier_vec[of _ n] have "?rhs = (∑p∈{p. p permutes ?n}. signof p * (∏i∈?n. ?m a c p i)) + (∑p∈{p. p permutes ?n}. signof p * (∏i∈?n. ?m b c p i))" unfolding det_def by simp also have "… = (∑p∈{p. p permutes ?n}. signof p * (∏i∈?n. ?m a c p i) + signof p * (∏i∈?n. ?m b c p i))" by (rule sum.distrib[symmetric]) also have "… = (∑p∈{p. p permutes ?n}. signof p * (∏i∈?n. ?m ?ab c p i))" proof (rule sum.cong, force) fix p assume "p ∈ {p. p permutes ?n}" hence p: "p permutes ?n" by simp show "signof p * (∏i∈?n. ?m a c p i) + signof p * (∏i∈?n. ?m b c p i) = signof p * (∏i∈?n. ?m ?ab c p i)" unfolding distrib_left[symmetric] proof (rule arg_cong[of _ _ "λ a. signof p * a"]) from k have f: "finite ?n" and k': "k ∈ ?n" by auto let ?nk = "?n - {k}" note split = prod.remove[OF f k'] have id1: "(∏i∈?n. ?m a c p i) = ?m a c p k * (∏i∈?nk. ?m a c p i)" by (rule split) have id2: "(∏i∈?n. ?m b c p i) = ?m b c p k * (∏i∈?nk. ?m b c p i)" by (rule split) have id3: "(∏i∈?n. ?m ?ab c p i) = ?m ?ab c p k * (∏i∈?nk. ?m ?ab c p i)" by (rule split) have id: "⋀ a. (∏i∈?nk. ?m a c p i) = (∏i∈?nk. ?c p i)" by (rule prod.cong, insert abc k p, auto intro!: intros) have ab: "?ab k ∈ carrier_vec n" using abc by (auto intro: intros) { fix f assume "f k ∈ (carrier_vec n :: 'a vec set)" hence "mat⇩_{r}n n (λi. if i = k then f i else c i) $$ (k, p k) = f k $ p k" by (insert p k abc, auto) } note first = this note id' = id1 id2 id3 have dist: "(a k + b k) $ p k = a k $ p k + b k $ p k" by (rule index_add_vec(1), insert p k abc, force) show "(∏i∈?n. ?m a c p i) + (∏i∈?n. ?m b c p i) = (∏i∈?n. ?m ?ab c p i)" unfolding id' id first[of a, OF abc(1)] first[of b, OF abc(2)] first[of ?ab, OF ab] dist by (rule distrib_right[symmetric]) qed qed also have "… = ?lhs" unfolding det_def by simp finally show ?thesis by simp qed lemma det_linear_row_finsum: assumes fS: "finite S" and c: "c ∈ {0..<n} → carrier_vec n" and k: "k < n" and a: "a k ∈ S → carrier_vec n" shows "det (mat⇩_{r}n n (λ i. if i = k then finsum_vec TYPE('a :: comm_ring_1) n (a i) S else c i)) = sum (λj. det (mat⇩_{r}n n (λ i. if i = k then a i j else c i))) S" proof - let ?sum = "finsum_vec TYPE('a) n" show ?thesis using a proof (induct rule: finite_induct[OF fS]) case 1 show ?case by (simp, unfold finsum_vec_empty, rule det_row_0[OF k c]) next case (2 x F) from 2(4) have ak: "a k ∈ F → carrier_vec n" and akx: "a k x ∈ carrier_vec n" by auto { fix i note if_cong[OF refl finsum_vec_insert[OF 2(1-2)], of _ "a i" n "c i" "c i"] } note * = this show ?case proof (subst *) show "det (mat⇩_{r}n n (λi. if i = k then a i x + ?sum (a i) F else c i)) = (∑j∈insert x F. det (mat⇩_{r}n n (λi. if i = k then a i j else c i)))" proof (subst det_row_add) show "det (mat⇩_{r}n n (λi. if i = k then a i x else c i)) + det (mat⇩_{r}n n (λi. if i = k then ?sum (a i) F else c i)) = (∑j∈insert x F. det (mat⇩_{r}n n (λi. if i = k then a i j else c i)))" unfolding 2(3)[OF ak] sum.insert[OF 2(1-2)] by simp qed (insert c k ak akx 2(1), auto intro!: finsum_vec_closed) qed (insert akx ak, force+) qed qed lemma det_linear_rows_finsum_lemma: assumes fS: "finite S" and fT: "finite T" and c: "c ∈ {0..<n} → carrier_vec n" and T: "T ⊆ {0 ..< n}" and a: "a ∈ T → S → carrier_vec n" shows "det (mat⇩_{r}n n (λ i. if i ∈ T then finsum_vec TYPE('a :: comm_ring_1) n (a i) S else c i)) = sum (λf. det(mat⇩_{r}n n (λ i. if i ∈ T then a i (f i) else c i))) {f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}" proof - let ?sum = "finsum_vec TYPE('a) n" show ?thesis using fT c a T proof (induct T arbitrary: a c set: finite) case empty let ?f = "(λ i. i) :: nat ⇒ nat" have [simp]: "{f. ∀i. f i = i} = {?f}" by auto show ?case by simp next case (insert z T a c) hence z: "z < n" and azS: "a z ∈ S → carrier_vec n" by auto let ?F = "λT. {f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}" let ?h = "λ(y,g) i. if i = z then y else g i" let ?k = "λh. (h(z),(λi. if i = z then i else h i))" let ?s = "λ k a c f. det(mat⇩_{r}n n (λ i. if i ∈ T then a i (f i) else c i))" let ?c = "λj i. if i = z then a i j else c i" have thif: "⋀a b c d. (if a ∨ b then c else d) = (if a then c else if b then c else d)" by simp have thif2: "⋀a b c d e. (if a then b else if c then d else e) = (if c then (if a then b else d) else (if a then b else e))" by simp from ‹z ∉ T› have nz: "⋀i. i ∈ T ⟹ i = z ⟷ False" by auto from insert have c: "⋀ i. i < n ⟹ c i ∈ carrier_vec n" by auto have fin: "finite {f. (∀i∈T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}" by (rule finite_bounded_functions[OF fS insert(1)]) have "det (mat⇩_{r}n n (λ i. if i ∈ insert z T then ?sum (a i) S else c i)) = det (mat⇩_{r}n n (λ i. if i = z then ?sum (a i) S else if i ∈ T then ?sum (a i) S else c i))" unfolding insert_iff thif .. also have "… = (∑j∈S. det (mat⇩_{r}n n (λ i. if i ∈ T then ?sum (a i) S else if i = z then a i j else c i)))" apply (subst det_linear_row_finsum[OF fS _ z]) prefer 3 apply (subst thif2) using nz apply (simp cong del: if_weak_cong cong add: if_cong) apply (insert azS c fS insert(5), (force intro!: finsum_vec_closed)+) done also have "… = (sum (λ (j, f). det (mat⇩_{r}n n (λ i. if i ∈ T then a i (f i) else if i = z then a i j else c i))) (S × ?F T))" unfolding sum.cartesian_product[symmetric] by (rule sum.cong[OF refl], subst insert.hyps(3), insert azS c fin z insert(5-6), auto) finally have tha: "det (mat⇩_{r}n n (λ i. if i ∈ insert z T then ?sum (a i) S else c i)) = (sum (λ (j, f). det (mat⇩_{r}n n (λ i. if i ∈ T then a i (f i) else if i = z then a i j else c i))) (S × ?F T))" . show ?case unfolding tha by (rule sum.reindex_bij_witness[where i="?k" and j="?h"], insert ‹z ∉ T› azS c fS insert(5-6) z fin, auto intro!: arg_cong[of _ _ det]) qed qed lemma det_linear_rows_sum: assumes fS: "finite S" and a: "a ∈ {0..<n} → S → carrier_vec n" shows "det (mat⇩_{r}n n (λ i. finsum_vec TYPE('a :: comm_ring_1) n (a i) S)) = sum (λf. det (mat⇩_{r}n n (λ i. a i (f i)))) {f. (∀i∈{0..<n}. f i ∈ S) ∧ (∀i. i ∉ {0..<n} ⟶ f i = i)}" proof - let ?T = "{0..<n}" have fT: "finite ?T" by auto have th0: "⋀x y. mat⇩_{r}n n (λ i. if i ∈ ?T then x i else y i) = mat⇩_{r}n n (λ i. x i)" by (rule eq_rowI, auto) have c: "(λ _. 0⇩_{v}n) ∈ ?T → carrier_vec n" by auto show ?thesis by (rule det_linear_rows_finsum_lemma[OF fS fT c subset_refl a, unfolded th0]) qed lemma det_rows_mul: assumes a: "a ∈ {0..<n} → carrier_vec n" shows "det(mat⇩_{r}n n (λ i. c i ⋅⇩_{v}a i)) = prod c {0..<n} * det(mat⇩_{r}n n (λ i. a i))" proof - have A: "mat⇩_{r}n n (λ i. c i ⋅⇩_{v}a i) ∈ carrier_mat n n" and A': "mat⇩_{r}n n (λ i. a i) ∈ carrier_mat n n" using a unfolding carrier_mat_def by auto show ?thesis unfolding det_def'[OF A] det_def'[OF A'] proof (rule trans[OF sum.cong sum_distrib_left[symmetric]]) fix p assume p: "p ∈ {p. p permutes {0..<n}}" have id: "(∏ia∈{0..<n}. mat⇩_{r}n n (λi. c i ⋅⇩_{v}a i) $$ (ia, p ia)) = prod c {0..<n} * (∏ia∈{0..<n}. mat⇩_{r}n n a $$ (ia, p ia))" unfolding prod.distrib[symmetric] by (rule prod.cong, insert p a, force+) show "signof p * (∏ia∈{0..<n}. mat⇩_{r}n n (λi. c i ⋅⇩_{v}a i) $$ (ia, p ia)) = prod c {0..<n} * (signof p * (∏ia∈{0..<n}. mat⇩_{r}n n a $$ (ia, p ia)))" unfolding id by auto qed simp qed lemma mat_mul_finsum_alt: assumes A: "A ∈ carrier_mat nr n" and B: "B ∈ carrier_mat n nc" shows "A * B = mat⇩_{r}nr nc (λ i. finsum_vec TYPE('a :: semiring_0) nc (λk. A $$ (i,k) ⋅⇩_{v}row B k) {0 ..< n})" by (rule eq_matI, insert A B, auto, subst index_finsum_vec, auto simp: scalar_prod_def intro: sum.cong) lemma det_mult: assumes A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" shows "det (A * B) = det A * det (B :: 'a :: comm_ring_1 mat)" proof - let ?U = "{0 ..< n}" let ?F = "{f. (∀i∈ ?U. f i ∈ ?U) ∧ (∀i. i ∉ ?U ⟶ f i = i)}" let ?PU = "{p. p permutes ?U}" have fU: "finite ?U" by blast have fF: "finite ?F" by (rule finite_bounded_functions, auto) { fix p assume p: "p permutes ?U" have "p ∈ ?F" unfolding mem_Collect_eq permutes_in_image[OF p] using p[unfolded permutes_def] by simp } then have PUF: "?PU ⊆ ?F" by blast { fix f assume fPU: "f ∈ ?F - ?PU" have fUU: "f ` ?U ⊆ ?U" using fPU by auto from fPU have f: "∀i ∈ ?U. f i ∈ ?U" "∀i. i ∉ ?U ⟶ f i = i" "¬(∀y. ∃!x. f x = y)" unfolding permutes_def by auto let ?A = "mat⇩_{r}n n (λ i. A $$ (i, f i) ⋅⇩_{v}row B (f i))" let ?B = "mat⇩_{r}n n (λ i. row B (f i))" have B': "?B ∈ carrier_mat n n" by (intro mat_row_carrierI) { assume fi: "inj_on f ?U" from inj_on_nat_permutes[OF fi] f have "f permutes ?U" by auto with fPU have False by simp } hence fni: "¬ inj_on f ?U" by auto then obtain i j where ij: "f i = f j" "i ≠ j" "i < n" "j < n" unfolding inj_on_def by auto from ij have rth: "row ?B i = row ?B j" by auto have "det ?A = 0" by (subst det_rows_mul, unfold det_identical_rows[OF B' ij(2-4) rth], insert f A B, auto) } then have zth: "⋀ f. f ∈ ?F - ?PU ⟹ det (mat⇩_{r}n n (λ i. A $$ (i, f i) ⋅⇩_{v}row B (f i))) = 0" by simp { fix p assume pU: "p ∈ ?PU" from pU have p: "p permutes ?U" by blast let ?s = "λp. (signof p) :: 'a" let ?f = "λq. ?s p * (∏ i∈ ?U. A $$ (i,p i)) * (?s q * (∏i∈ ?U. B $$ (i, q i)))" have "(sum (λq. ?s q * (∏i∈ ?U. mat⇩_{r}n n (λ i. A $$ (i, p i) ⋅⇩_{v}row B (p i)) $$ (i, q i))) ?PU) = (sum (λq. ?s p * (∏ i∈ ?U. A $$ (i,p i)) * (?s q * (∏ i∈ ?U. B $$ (i, q i)))) ?PU)" unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] proof (rule sum.cong[OF refl]) fix q assume "q ∈ {q. q permutes ?U}" hence q: "q permutes ?U" by simp from p q have pp: "permutation p" and pq: "permutation q" unfolding permutation_permutes by auto note sign = signof_compose[OF q permutes_inv[OF p], unfolded signof_inv[OF fU p]] let ?inv = "Hilbert_Choice.inv" have th001: "prod (λi. B$$ (i, q (?inv p i))) ?U = prod ((λi. B$$ (i, q (?inv p i))) ∘ p) ?U" by (rule prod.permute[OF p]) have thp: "prod (λi. mat⇩_{r}n n (λ i. A$$(i,p i) ⋅⇩_{v}row B (p i)) $$ (i, q i)) ?U = prod (λi. A$$(i,p i)) ?U * prod (λi. B$$ (i, q (?inv p i))) ?U" unfolding th001 o_def permutes_inverses[OF p] by (subst prod.distrib[symmetric], insert A p q B, auto intro: prod.cong) define AA where "AA = (∏i∈?U. A $$ (i, p i))" define BB where "BB = (∏ia∈{0..<n}. B $$ (ia, q (?inv p ia)))" have "?s q * (∏ia∈{0..<n}. mat⇩_{r}n n (λi. A $$ (i, p i) ⋅⇩_{v}row B (p i)) $$ (ia, q ia)) = ?s p * (∏i∈{0..<n}. A $$ (i, p i)) * (?s (q ∘ ?inv p) * (∏ia∈{0..<n}. B $$ (ia, q (?inv p ia))))" unfolding sign thp unfolding AA_def[symmetric] BB_def[symmetric] by (simp add: ac_simps flip: of_int_mult) thus "?s q * (∏i = 0..<n. mat⇩_{r}n n (λi. A $$ (i, p i) ⋅⇩_{v}row B (p i)) $$ (i, q i)) = ?s p * (∏i = 0..<n. A $$ (i, p i)) * (?s (q ∘ ?inv p) * (∏i = 0..<n. B $$ (i, (q ∘ ?inv p) i)))" by simp qed } note * = this have th2: "sum (λf. det (mat⇩_{r}n n (λ i. A$$(i,f i) ⋅⇩_{v}row B (f i)))) ?PU = det A * det B" unfolding det_def'[OF A] det_def'[OF B] det_def'[OF mat_row_carrierI] unfolding sum_product dim_row_mat by (rule sum.cong, insert A, force, subst *, insert A B, auto) let ?f = "λ f. det (mat⇩_{r}n n (λ i. A $$ (i, f i) ⋅⇩_{v}row B (f i)))" have "det (A * B) = sum ?f ?F" unfolding mat_mul_finsum_alt[OF A B] by (rule det_linear_rows_sum[OF fU], insert A B, auto) also have "… = sum ?f ((?F - ?PU) ∪ (?F ∩ ?PU))" by (rule arg_cong[where f = "sum ?f"], auto) also have "… = sum ?f (?F - ?PU) + sum ?f (?F ∩ ?PU)" by (rule sum.union_disjoint, insert A B finite_bounded_functions[OF fU fU], auto) also have "sum ?f (?F - ?PU) = 0" by (rule sum.neutral, insert zth, auto) also have "?F ∩ ?PU = ?PU" unfolding permutes_def by fastforce also have "sum ?f ?PU = det A * det B" unfolding th2 .. finally show ?thesis by simp qed lemma unit_imp_det_non_zero: assumes "A ∈ Units (ring_mat TYPE('a :: comm_ring_1) n b)" shows "det A ≠ 0" proof - from assms[unfolded Units_def ring_mat_def] obtain B where A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" and BA: "B * A = 1⇩_{m}n" by auto from arg_cong[OF BA, of det, unfolded det_mult[OF B A] det_one] show ?thesis by auto qed text ‹The following proof is based on the Gauss-Jordan algorithm.› lemma det_non_zero_imp_unit: assumes A: "A ∈ carrier_mat n n" and dA: "det A ≠ (0 :: 'a :: field)" shows "A ∈ Units (ring_mat TYPE('a) n b)" proof (rule ccontr) let ?g = "gauss_jordan A (0⇩_{m}n 0)" let ?B = "fst ?g" obtain B C where B: "?g = (B,C)" by (cases ?g) assume "¬ ?thesis" from this[unfolded gauss_jordan_check_invertable[OF A zero_carrier_mat[of n 0]] B] have "B ≠ 1⇩_{m}n" by auto with row_echelon_form_imp_1_or_0_row[OF gauss_jordan_carrier(1)[OF A _ B] gauss_jordan_row_echelon[OF A B], of 0] have n: "0 < n" and row: "row B (n - 1) = 0⇩_{v}n" by auto let ?n = "n - 1" from n have n1: "?n < n" by auto from gauss_jordan_transform[OF A _ B, of 0 b] obtain P where P: "P∈Units (ring_mat TYPE('a) n b)" and PA: "B = P * A" by auto from unit_imp_det_non_zero[OF P] have dP: "det P ≠ 0" by auto from P have P: "P ∈ carrier_mat n n" unfolding Units_def ring_mat_def by auto from det_mult[OF P A] dP dA have "det B ≠ 0" unfolding PA by simp also have "det B = 0" proof - from gauss_jordan_carrier[OF A _ B, of 0] have B: "B ∈ carrier_mat n n" by auto { fix j assume j: "j < n" from index_row(1)[symmetric, of ?n B j, unfolded row] B have "B $$ (?n, j) = 0" using B n j by auto } hence "B = mat⇩_{r}n n (λi. if i = ?n then 0⇩_{v}n else row B i)" by (intro eq_matI, insert B, auto) also have "det … = 0" by (rule det_row_0[OF n1], insert B, auto) finally show "det B = 0" . qed finally show False by simp qed lemma mat_mult_left_right_inverse: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" and AB: "A * B = 1⇩_{m}n" shows "B * A = 1⇩_{m}n" proof - let ?R = "ring_mat TYPE('a) n undefined" from det_mult[OF A B, unfolded AB] have "det A ≠ 0" "det B ≠ 0" by auto from det_non_zero_imp_unit[OF A this(1)] det_non_zero_imp_unit[OF B this(2)] have U: "A ∈ Units ?R" "B ∈ Units ?R" . interpret ring ?R by (rule ring_mat) from Units_inv_comm[unfolded ring_mat_simps, OF AB U] show ?thesis . qed lemma det_zero_imp_zero_row: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n" and det: "det A = 0" shows "∃ P. P ∈ Units (ring_mat TYPE('a) n b) ∧ row (P * A) (n - 1) = 0⇩_{v}n ∧ 0 < n ∧ row_echelon_form (P * A)" proof - let ?R = "ring_mat TYPE('a) n b" let ?U = "Units ?R" interpret m: ring ?R by (rule ring_mat) let ?g = "gauss_jordan A A" obtain A' B' where g: "?g = (A', B')" by (cases ?g) from det unit_imp_det_non_zero[of A n b] have AU: "A ∉ ?U" by auto with gauss_jordan_inverse_one_direction(1)[OF A A, of _ b] have A'1: "A' ≠ 1⇩_{m}n" using g by auto from gauss_jordan_carrier(1)[OF A A g] have A': "A' ∈ carrier_mat n n" by auto from gauss_jordan_row_echelon[OF A g] have re: "row_echelon_form A'" . from row_echelon_form_imp_1_or_0_row[OF A' this] A'1 have n: "0 < n" and row: "row A' (n - 1) = 0⇩_{v}n" by auto from gauss_jordan_transform[OF A A g, of b] obtain P where P: "P ∈ ?U" and A': "A' = P * A" by auto thus ?thesis using n row re by auto qed lemma det_0_iff_vec_prod_zero_field: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n" shows "det A = 0 ⟷ (∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩_{v}n ∧ A *⇩_{v}v = 0⇩_{v}n)" (is "?l = (∃ v. ?P v)") proof - let ?R = "ring_mat TYPE('a) n ()" let ?U = "Units ?R" interpret m: ring ?R by (rule ring_mat) show ?thesis proof (cases "det A = 0") case False from det_non_zero_imp_unit[OF A this, of "()"] have "A ∈ ?U" . then obtain B where unit: "B * A = 1⇩_{m}n" and B: "B ∈ carrier_mat n n" unfolding Units_def ring_mat_def by auto { fix v assume "?P v" hence v: "v ∈ carrier_vec n" "v ≠ 0⇩_{v}n" "A *⇩_{v}v = 0⇩_{v}n" by auto have "v = (B * A) *⇩_{v}v" using v B unfolding unit by auto also have "… = B *⇩_{v}(A *⇩_{v}v)" using B A v by simp also have "… = B *⇩_{v}0⇩_{v}n" unfolding v .. also have "… = 0⇩_{v}n" using B by auto finally have False using v by simp } with False show ?thesis by blast next case True let ?n = "n - 1" from det_zero_imp_zero_row[OF A True, of "()"] obtain P where PU: "P ∈ ?U" and row: "row (P * A) ?n = 0⇩_{v}n" and n: "0 < n" "?n < n" and re: "row_echelon_form (P * A)" by auto define PA where "PA = P * A" note row = row[folded PA_def] note re = re[folded PA_def] from PU obtain Q where P: "P ∈ carrier_mat n n" and Q: "Q ∈ carrier_mat n n" and unit: "Q * P = 1⇩_{m}n" "P * Q = 1⇩_{m}n" unfolding Units_def ring_mat_def by auto from P A have PA: "PA ∈ carrier_mat n n" and dimPA: "dim_row PA = n" unfolding PA_def by auto from re[unfolded row_echelon_form_def] obtain p where p: "pivot_fun PA p n" using PA by auto note piv = pivot_positions[OF PA p] note pivot = pivot_funD[OF dimPA p n(2)] { assume "p ?n < n" with pivot(4)[OF this] n arg_cong[OF row, of "λ v. v $ p ?n"] have False using PA by auto } with pivot(1) have pn: "p ?n = n" by fastforce with piv(1) have "set (pivot_positions PA) ⊆ {(i, p i) |i. i < n ∧ p i ≠ n} - {(?n,p ?n)}" by auto also have "… ⊆ {(i, p i) | i. i < ?n}" using n by force finally have "card (set (pivot_positions PA)) ≤ card {(i, p i) | i. i < ?n}" by (intro card_mono, auto) also have "{(i, p i) | i. i < ?n} = (λ i. (i, p i)) ` {0 ..< ?n}" by auto also have "card … = card {0 ..< ?n}" by (rule card_image, auto simp: inj_on_def) also have "… < n" using n by simp finally have "card (set (pivot_positions PA)) < n" . hence "card (snd ` (set (pivot_positions PA))) < n" using card_image_le[OF finite_set, of snd "pivot_positions PA"] by auto hence neq: "snd ` (set (pivot_positions PA)) ≠ {0 ..< n}" by auto from find_base_vector[OF re PA neq] obtain v where v: "v ∈ carrier_vec n" and v0: "v ≠ 0⇩_{v}n" and pav: "PA *⇩_{v}v = 0⇩_{v}n" by auto have "A *⇩_{v}v = Q * P *⇩_{v}(A *⇩_{v}v)" unfolding unit using A v by auto also have "… = Q *⇩_{v}(PA *⇩_{v}v)" unfolding PA_def using Q P A v by auto also have "PA *⇩_{v}v = 0⇩_{v}n" unfolding pav .. also have "Q *⇩_{v}0⇩_{v}n = 0⇩_{v}n" using Q by auto finally have Av: "A *⇩_{v}v = 0⇩_{v}n" by auto show ?thesis unfolding True using Av v0 v by auto qed qed text ‹In order to get the result for integral domains, we embed the domain in its fraction field, and then apply the result for fields.› lemma det_0_iff_vec_prod_zero: assumes A: "(A :: 'a :: idom mat) ∈ carrier_mat n n" shows "det A = 0 ⟷ (∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩_{v}n ∧ A *⇩_{v}v = 0⇩_{v}n)" proof - let ?h = "to_fract :: 'a ⇒ 'a fract" let ?A = "map_mat ?h A" have A': "?A ∈ carrier_mat n n" using A by auto interpret inj_comm_ring_hom ?h by (unfold_locales, auto) have "(det A = 0) = (?h (det A) = ?h 0)" by auto also have "… = (det ?A = 0)" unfolding hom_zero hom_det .. also have "… = ((∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩_{v}n ∧ ?A *⇩_{v}v = 0⇩_{v}n))" unfolding det_0_iff_vec_prod_zero_field[OF A'] .. also have "… = ((∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩_{v}n ∧ A *⇩_{v}v = 0⇩_{v}n))" (is "?l = ?r") proof assume ?r then obtain v where v: "v ∈ carrier_vec n" "v ≠ 0⇩_{v}n" "A *⇩_{v}v = 0⇩_{v}n" by auto show ?l by (rule exI[of _ "map_vec ?h v"], insert v, auto simp: mult_mat_vec_hom[symmetric, OF A v(1)]) next assume ?l then obtain v where v: "v ∈ carrier_vec n" and v0: "v ≠ 0⇩_{v}n" and Av: "?A *⇩_{v}v = 0⇩_{v}n" by auto have "∀ i. ∃ a b. v $ i = Fraction_Field.Fract a b ∧ b ≠ 0" using Fract_cases[of "v $ i" for i] by metis from choice[OF this] obtain a where "∀ i. ∃ b. v $ i = Fraction_Field.Fract (a i) b ∧ b ≠ 0" by metis from choice[OF this] obtain b where vi: "⋀ i. v $ i = Fraction_Field.Fract (a i) (b i)" and bi: "⋀ i. b i ≠ 0" by auto define m where "m = prod_list (map b [0..<n])" let ?m = "?h m" have m0: "m ≠ 0" unfolding m_def hom_0_iff prod_list_zero_iff using bi by auto from v0[unfolded vec_eq_iff] v obtain i where i: "i < n" "v $ i ≠ 0" by auto { fix i assume "i < n" hence "b i ∈ set (map b [0 ..< n])" by auto from split_list[OF this] obtain ys zs where "map b [0..<n] = ys @ b i # zs" by auto hence "b i dvd m" unfolding m_def by auto then obtain c where "m = b i * c" .. hence "?m * v $ i = ?h (a i * c)" unfolding vi using bi[of i] by (simp add: eq_fract to_fract_def) hence "∃ c. ?m * v $ i = ?h c" .. } hence "∀ i. ∃ c. i < n ⟶ ?m * v $ i = ?h c" by auto from choice[OF this] obtain c where c: "⋀ i. i < n ⟹ ?m * v $ i = ?h (c i)" by auto define w where "w = vec n c" have w: "w ∈ carrier_vec n" unfolding w_def by simp have mvw: "?m ⋅⇩_{v}v = map_vec ?h w" unfolding w_def using c v by (intro eq_vecI, auto) with m0 i c[OF i(1)] have "w $ i ≠ 0" unfolding w_def by auto with i w have w0: "w ≠ 0⇩_{v}n" by auto from arg_cong[OF Av, of "λ v. ?m ⋅⇩_{v}v"] have "?m ⋅⇩_{v}(?A *⇩_{v}v) = map_vec ?h (0⇩_{v}n)" by auto also have "?m ⋅⇩_{v}(?A *⇩_{v}v) = ?A *⇩_{v}(?m ⋅⇩_{v}v)" using A v by auto also have "… = ?A *⇩_{v}(map_vec ?h w)" unfolding mvw .. also have "… = map_vec ?h (A *⇩_{v}w)" unfolding mult_mat_vec_hom[OF A w] .. finally have "A *⇩_{v}w = 0⇩_{v}n" by (rule vec_hom_inj) with w w0 show ?r by blast qed finally show ?thesis . qed lemma det_0_negate: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n" shows "(det (- A) = 0) = (det A = 0)" proof - from A have mA: "- A ∈ carrier_mat n n" by auto { fix v :: "'a vec" assume v: "v ∈ carrier_vec n" hence Av: "A *⇩_{v}v ∈ carrier_vec n" using A by auto have id: "- A *⇩_{v}v = - (A *⇩_{v}v)" using v A by simp have "(- A *⇩_{v}v = 0⇩_{v}n) = (A *⇩_{v}v = 0⇩_{v}n)" unfolding id unfolding uminus_zero_vec_eq[OF Av] .. } thus ?thesis unfolding det_0_iff_vec_prod_zero[OF A] det_0_iff_vec_prod_zero[OF mA] by auto qed lemma det_multrow: assumes k: "k < n" and A: "A ∈ carrier_mat n n" shows "det (multrow k a A) = a * det A" proof - have "multrow k a A = multrow_mat n k a * A" by (rule multrow_mat[OF A]) also have "det (multrow_mat n k a * A) = det (multrow_mat n k a) * det A" by (rule det_mult[OF _ A], auto) also have "det (multrow_mat n k a) = a" by (rule det_multrow_mat[OF k]) finally show ?thesis . qed lemma det_multrow_div: assumes k: "k < n" and A: "A ∈ carrier_mat n n" and a0: "a ≠ 0" shows "det (multrow k a A :: 'a :: idom_divide mat) div a = det A" proof - have "det (multrow k a A) div a = a * det A div a" using k A by (simp add: det_multrow) also have "... = det A" using a0 by auto finally show ?thesis. qed lemma det_addrow: assumes l: "l < n" and k: "k ≠ l" and A: "A ∈ carrier_mat n n" shows "det (addrow a k l A) = det A" proof - have "addrow a k l A = addrow_mat n a k l * A" by (rule addrow_mat[OF A l]) also have "det (addrow_mat n a k l * A) = det (addrow_mat n a k l) * det A" by (rule det_mult[OF _ A], auto) also have "det (addrow_mat n a k l) = 1" by (rule det_addrow_mat[OF k]) finally show ?thesis using A by simp qed lemma det_swaprows: assumes *: "k < n" "l < n" and k: "k ≠ l" and A: "A ∈ carrier_mat n n" shows "det (swaprows k l A) = - det A" proof - have "swaprows k l A = swaprows_mat n k l * A" by (rule swaprows_mat[OF A *]) also have "det (swaprows_mat n k l * A) = det (swaprows_mat n k l) * det A" by (rule det_mult[OF _ A], insert A, auto) also have "det (swaprows_mat n k l) = - 1" by (rule det_swaprows_mat[OF * k]) finally show ?thesis using A by simp qed lemma det_similar: assumes "similar_mat A B" shows "det A = det B" proof - from similar_matD[OF assms] obtain n P Q where carr: "{A, B, P, Q} ⊆ carrier_mat n n" (is "_ ⊆ ?C") and PQ: "P * Q = 1⇩_{m}n" and AB: "A = P * B * Q" by blast hence A: "A ∈ ?C" and B: "B ∈ ?C" and P: "P ∈ ?C" and Q: "Q ∈ ?C" by auto from det_mult[OF P Q, unfolded PQ] have PQ: "det P * det Q = 1" by auto from det_mult[OF _ Q, of "P * B", unfolded det_mult[OF P B] AB[symmetric]] P B have "det A = det P * det B * det Q" by auto also have "… = (det P * det Q) * det B" by (simp add: ac_simps) also have "… = det B" unfolding PQ by simp finally show ?thesis . qed lemma det_four_block_mat_upper_right_zero_col: assumes A1: "A1 ∈ carrier_mat n n" and A20: "A2 = (0⇩_{m}n 1)" and A3: "A3 ∈ carrier_mat 1 n" and A4: "A4 ∈ carrier_mat 1 1" shows "det (four_block_mat A1 A2 A3 A4) = det A1 * det A4" (is "det ?A = _") proof - let ?A = "four_block_mat A1 A2 A3 A4" from A20 have A2: "A2 ∈ carrier_mat n 1" by auto define A where "A = ?A" from four_block_carrier_mat[OF A1 A4] A1 have A: "A ∈ carrier_mat (Suc n) (Suc n)" and dim: "dim_row A1 = n" unfolding A_def by auto let ?Pn = "λ p. p permutes {0 ..< n}" let ?Psn = "λ p. p permutes {0 ..< Suc n}" let ?perm = "{p. ?Psn p}" let ?permn = "{p. ?Pn p}" let ?prod = "λ p. signof p * (∏i = 0..<Suc n. A $$ (p i, i))" let ?prod' = "λ p. A $$ (p n, n) * signof p * (∏i = 0..<n. A $$ (p i, i))" let ?prod'' = "λ p. signof p * (∏i = 0..< n. A $$ (p i, i))" let ?prod''' = "λ p. signof p * (∏i = 0..< n. A1 $$ (p i, i))" let ?p0 = "{p. p 0 = 0}" have [simp]: "{0..<Suc n} - {n} = {0..< n}" by auto { fix p assume "?Psn p" have "?prod p = signof p * (A $$ (p n, n) * (∏ i ∈ {0..< n}. A $$ (p i, i)))" by (subst prod.remove[of _ n], auto) also have "… = A $$ (p n, n) * signof p * (∏ i ∈ {0..< n}. A $$ (p i, i))" by simp finally have "?prod p = ?prod' p" . } note prod_id = this define prod' where "prod' = ?prod'" { fix i q assume i: "i ∈ {0..< n}" "q permutes {0 ..< n}" hence "Fun.swap n i id (q n) < n" unfolding permutes_def by auto hence "A $$ (Fun.swap n i id (q n), n) = 0" unfolding A_def using A1 A20 A3 A4 by auto hence "prod' (Fun.swap n i id ∘ q) = 0" unfolding prod'_def by simp } note zero = this have cong: "⋀ a b c. b = c ⟹ a * b = a * c" by auto have "det ?A = sum ?prod ?perm" unfolding A_def[symmetric] using mat_det_left_def[OF A] A by simp also have "… = sum prod' ?perm" unfolding prod'_def by (rule sum.cong[OF refl], insert prod_id, auto) also have "{0 ..< Suc n} = insert n {0 ..< n}" by auto also have "sum prod' {p. p permutes …} = (∑i∈insert n {0..<n}. ∑q∈?permn. prod' (Fun.swap n i id ∘ q))" by (subst sum_over_permutations_insert, auto) also have "… = (∑q∈?permn. prod' q) + (∑i∈{0..<n}. ∑q∈?permn. prod' (Fun.swap n i id ∘ q))" by (subst sum.insert, auto) also have "(∑i∈{0..<n}. ∑q∈?permn. prod' (Fun.swap n i id ∘ q)) = 0" by (rule sum.neutral, intro ballI, rule sum.neutral, intro ballI, rule zero, auto) also have "(∑q∈ ?permn. prod' q) = A $$ (n,n) * (∑q∈ ?permn. ?prod'' q)" unfolding prod'_def by (subst sum_distrib_left, rule sum.cong[OF refl], auto simp: permutes_def ac_simps) also have "A $$ (n,n) = A4 $$ (0,0)" unfolding A_def using A1 A2 A3 A4 by auto also have "(∑q∈ ?permn. ?prod'' q) = (∑q∈ ?permn. ?prod''' q)" by (rule sum.cong[OF refl], rule cong, rule prod.cong, insert A1 A2 A3 A4, auto simp: permutes_def A_def) also have "… = det A1" unfolding mat_det_left_def[OF A1] dim by auto also have "A4 $$ (0,0) = det A4" using A4 unfolding det_def[of A4] by (auto simp: sign_def) finally show ?thesis by simp qed lemma det_swap_initial_rows: assumes A: "A ∈ carrier_mat m m" and lt: "k + n ≤ m" shows "det A = (- 1) ^ (k * n) * det (mat m m (λ(i, j). A $$ (if i < n then i + k else if i < k + n then i - n else i, j)))" proof - define sw where "sw = (λ (A :: 'a mat) xs. fold (λ (i,j). swaprows i j) xs A)" have dim_sw[simp]: "dim_row (sw A xs) = dim_row A" "dim_col (sw A xs) = dim_col A" for xs A unfolding sw_def by (induct xs arbitrary: A, auto) { fix xs and A :: "'a mat" assume "dim_row A = dim_col A" "⋀ i j. (i,j) ∈ set xs ⟹ i < dim_col A ∧ j < dim_col A ∧ i ≠ j" hence "det (sw A xs) = (-1)^(length xs) * det A" unfolding sw_def proof (induct xs arbitrary: A) case (Cons xy xs A) obtain x y where xy: "xy = (x,y)" by force from Cons(3)[unfolded xy, of x y] Cons(2) have [simp]: "det (swaprows x y A) = - det A" by (intro det_swaprows, auto) show ?case unfolding xy by (simp, insert Cons(2-), (subst Cons(1), auto)+) qed simp } note sw = this define swb where "swb = (λ A i n. sw A (map (λ j. (j,Suc j)) [i ..< i + n]))" { fix k n and A :: "'a mat" assume k_n: "k + n < dim_row A" hence "swb A k n = mat (dim_row A) (dim_col A) (λ (i,j). let r = (if i < k ∨ i > k + n then i else if i = k + n then k else Suc i) in A $$ (r,j))" proof (induct n) case 0 show ?case unfolding swb_def sw_def by (rule eq_matI, auto) next case (Suc n) hence dim: "k + n < dim_row A" by auto have id: "swb A k (Suc n) = swaprows (k + n) (Suc k + n) (swb A k n)" unfolding swb_def sw_def by simp show ?case unfolding id Suc(1)[OF dim] by (rule eq_matI, insert Suc(2), auto) qed } note swb = this define swbl where "swbl = (λ A k n. fold (λ i A. swb A i n) (rev [0 ..< k]) A)" { fix k n and A :: "'a mat" assume k_n: "k + n ≤ dim_row A" hence "swbl A k n = mat (dim_row A) (dim_col A) (λ (i,j). let r = (if i < n then i + k else if i < k + n then i - n else i) in A $$ (r,j))" proof (induct k arbitrary: A) case 0 thus ?case unfolding swbl_def by (intro eq_matI, auto simp: swb) next case (Suc k) hence dim: "k + n < dim_row A" by auto have id: