generalized Cramer's rule
authorimmler
Thu May 24 17:06:39 2018 +0200 (21 months ago)
changeset 68263e4e536a71e3d
parent 68262 d231238bd977
child 68269 5ff0ccc74884
child 68282 d6b789072d72
generalized Cramer's rule
src/HOL/Analysis/Determinants.thy
     1.1 --- a/src/HOL/Analysis/Determinants.thy	Thu May 24 16:38:24 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Determinants.thy	Thu May 24 17:06:39 2018 +0200
     1.3 @@ -864,10 +864,10 @@
     1.4  subsection \<open>Cramer's rule\<close>
     1.5  
     1.6  lemma cramer_lemma_transpose:
     1.7 -  fixes A:: "real^'n^'n"
     1.8 -    and x :: "real^'n"
     1.9 +  fixes A:: "'a::{field}^'n^'n"
    1.10 +    and x :: "'a::{field}^'n"
    1.11    shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
    1.12 -                             else row i A)::real^'n^'n) = x$k * det A"
    1.13 +                             else row i A)::'a::{field}^'n^'n) = x$k * det A"
    1.14    (is "?lhs = ?rhs")
    1.15  proof -
    1.16    let ?U = "UNIV :: 'n set"
    1.17 @@ -900,8 +900,8 @@
    1.18  qed
    1.19  
    1.20  lemma cramer_lemma:
    1.21 -  fixes A :: "real^'n^'n"
    1.22 -  shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: real^'n^'n) = x$k * det A"
    1.23 +  fixes A :: "'a::{field}^'n^'n"
    1.24 +  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"
    1.25  proof -
    1.26    let ?U = "UNIV :: 'n set"
    1.27    have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"
    1.28 @@ -917,7 +917,7 @@
    1.29  qed
    1.30  
    1.31  lemma cramer:
    1.32 -  fixes A ::"real^'n^'n"
    1.33 +  fixes A ::"'a::{field}^'n^'n"
    1.34    assumes d0: "det A \<noteq> 0"
    1.35    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)"
    1.36  proof -