# Theory Jordan_Normal_Form.Determinant

(*
Author:      René Thiemann
*)
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"
{
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]
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

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
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

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: "