# HG changeset patch # User immler # Date 1527174399 -7200 # Node ID e4e536a71e3dcc205b974a50282a0509a76c9a99 # Parent d231238bd977ca830aa52079200b7ce44c2acdf2 generalized Cramer's rule diff -r d231238bd977 -r e4e536a71e3d src/HOL/Analysis/Determinants.thy --- a/src/HOL/Analysis/Determinants.thy Thu May 24 16:38:24 2018 +0200 +++ b/src/HOL/Analysis/Determinants.thy Thu May 24 17:06:39 2018 +0200 @@ -864,10 +864,10 @@ subsection \Cramer's rule\ lemma cramer_lemma_transpose: - fixes A:: "real^'n^'n" - and x :: "real^'n" + fixes A:: "'a::{field}^'n^'n" + and x :: "'a::{field}^'n" shows "det ((\ i. if i = k then sum (\i. x\$i *s row i A) (UNIV::'n set) - else row i A)::real^'n^'n) = x\$k * det A" + else row i A)::'a::{field}^'n^'n) = x\$k * det A" (is "?lhs = ?rhs") proof - let ?U = "UNIV :: 'n set" @@ -900,8 +900,8 @@ qed lemma cramer_lemma: - fixes A :: "real^'n^'n" - shows "det((\ i j. if j = k then (A *v x)\$i else A\$i\$j):: real^'n^'n) = x\$k * det A" + fixes A :: "'a::{field}^'n^'n" + shows "det((\ i j. if j = k then (A *v x)\$i else A\$i\$j):: 'a::{field}^'n^'n) = x\$k * det A" proof - let ?U = "UNIV :: 'n set" have *: "\c. sum (\i. c i *s row i (transpose A)) ?U = sum (\i. c i *s column i A) ?U" @@ -917,7 +917,7 @@ qed lemma cramer: - fixes A ::"real^'n^'n" + fixes A ::"'a::{field}^'n^'n" assumes d0: "det A \ 0" shows "A *v x = b \ x = (\ k. det(\ i j. if j=k then b\$i else A\$i\$j) / det A)" proof -