src/HOL/Analysis/Determinants.thy
 changeset 68263 e4e536a71e3d parent 68143 58c9231c2937 child 68833 fde093888c16
equal inserted replaced
68262:d231238bd977 68263:e4e536a71e3d
`   862 `
`   862 `
`   863 `
`   863 `
`   864 subsection \<open>Cramer's rule\<close>`
`   864 subsection \<open>Cramer's rule\<close>`
`   865 `
`   865 `
`   866 lemma cramer_lemma_transpose:`
`   866 lemma cramer_lemma_transpose:`
`   867   fixes A:: "real^'n^'n"`
`   867   fixes A:: "'a::{field}^'n^'n"`
`   868     and x :: "real^'n"`
`   868     and x :: "'a::{field}^'n"`
`   869   shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x\$i *s row i A) (UNIV::'n set)`
`   869   shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x\$i *s row i A) (UNIV::'n set)`
`   870                              else row i A)::real^'n^'n) = x\$k * det A"`
`   870                              else row i A)::'a::{field}^'n^'n) = x\$k * det A"`
`   871   (is "?lhs = ?rhs")`
`   871   (is "?lhs = ?rhs")`
`   872 proof -`
`   872 proof -`
`   873   let ?U = "UNIV :: 'n set"`
`   873   let ?U = "UNIV :: 'n set"`
`   874   let ?Uk = "?U - {k}"`
`   874   let ?Uk = "?U - {k}"`
`   875   have U: "?U = insert k ?Uk"`
`   875   have U: "?U = insert k ?Uk"`
`   898     apply (simp add: field_simps)`
`   898     apply (simp add: field_simps)`
`   899     done`
`   899     done`
`   900 qed`
`   900 qed`
`   901 `
`   901 `
`   902 lemma cramer_lemma:`
`   902 lemma cramer_lemma:`
`   903   fixes A :: "real^'n^'n"`
`   903   fixes A :: "'a::{field}^'n^'n"`
`   904   shows "det((\<chi> i j. if j = k then (A *v x)\$i else A\$i\$j):: real^'n^'n) = x\$k * det A"`
`   904   shows "det((\<chi> i j. if j = k then (A *v x)\$i else A\$i\$j):: 'a::{field}^'n^'n) = x\$k * det A"`
`   905 proof -`
`   905 proof -`
`   906   let ?U = "UNIV :: 'n set"`
`   906   let ?U = "UNIV :: 'n set"`
`   907   have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"`
`   907   have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"`
`   908     by (auto intro: sum.cong)`
`   908     by (auto intro: sum.cong)`
`   909   show ?thesis`
`   909   show ?thesis`
`   915     apply (vector transpose_def column_def row_def)`
`   915     apply (vector transpose_def column_def row_def)`
`   916     done`
`   916     done`
`   917 qed`
`   917 qed`
`   918 `
`   918 `
`   919 lemma cramer:`
`   919 lemma cramer:`
`   920   fixes A ::"real^'n^'n"`
`   920   fixes A ::"'a::{field}^'n^'n"`
`   921   assumes d0: "det A \<noteq> 0"`
`   921   assumes d0: "det A \<noteq> 0"`
`   922   shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j) / det A)"`
`   922   shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j) / det A)"`
`   923 proof -`
`   923 proof -`
`   924   from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"`
`   924   from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"`
`   925     unfolding invertible_det_nz[symmetric] invertible_def`
`   925     unfolding invertible_det_nz[symmetric] invertible_def`