1

我最近开始使用伊莎贝尔定理证明器。因为我想证明另一个引理，所以我想使用与引理“det_linear_row_setsum”中使用的符号不同的符号，它可以在 HOL 库中找到。更具体地说，我想使用“χ ij notation”而不是“χ i”。一段时间以来，我一直在尝试制定一个等效的表达式，但还没有弄清楚。

(* ORIGINAL lemma from library *)
(* from HOL/Multivariate_Analysis/Determinants.thy *)
lemma det_linear_row_setsum:
  assumes fS: "finite S"
  shows "det ((χ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (λj. det ((χ i. if i = k then a  i j else c i)::'a^'n^'n)) S"
proof(induct rule: finite_induct[OF fS])
  case 1 thus ?case apply simp  unfolding setsum_empty det_row_0[of k] ..
next
  case (2 x F)
  then  show ?case by (simp add: det_row_add cong del: if_weak_cong)
qed

..

(* My approach to rewrite the above lemma in χ i j matrix notation *)
lemma mydet_linear_row_setsum:
  assumes fS: "finite S"
  fixes A :: "'a::comm_ring_1^'n^'n" and k :: "'n"  and vec1 :: "'vec1 ⇒ ('a, 'n) vec"
  shows "det ( χ r c . if r = k then (setsum (λj .vec1 j $ c) S) else A $ r $ c ) =
    (setsum (λj . (det( χ r c . if r = k then vec1 j $ c else A $ r $ c ))) S)" 
proof-
  show ?thesis sorry
qed
4

1 回答 1

2

首先，让自己清楚原始引理所说的内容：a是由i和索引的向量族j，c是由 索引的向量族i。k左边矩阵的第 - 行是集合中a k j所有向量的总和。其他行取自. 在右边，矩阵是相同的，除了 row是 now并且 the被绑定在外部总和中。jScka k jj

正如您所意识到的，向量族a仅用于索引i = k，因此您可以替换a为%_ j. vec1 $ j。您的矩阵A产生行族，即c变为%r. A $ r。然后，您只需要利用该（(χ n. x $ n) = x定理vec_nth_inverse）并推动and 。结果如下所示：$ifsetsum

lemma mydet_linear_row_setsum:
  assumes fS: "finite S"
  fixes A :: "'a::comm_ring_1^'n^'n" and k :: "'n" and vec1 :: "'vec1 => 'a^'n"
  shows "det (χ r c . if r = k then setsum (%j. vec1 j $ c) S else A $ r $ c) =
    (setsum (%j. (det(χ r c . if r = k then vec1 j $ c else A $ r $ c))) S)"

为了证明这一点，您只需要撤消扩展和推动，引理if_distrib,cond_application_beta和setsum_component可能会帮助您这样做。

于 2013-06-26T11:25:28.110 回答