伊莎貝爾：矩陣轉置，包括一個常數因子

Question

在我的伊莎貝爾理論上我有一個常數因子矩陣：

... 
k :: 'n and c :: 'a 
(χ i j. if j = k then c * (A $ i $ j) else A $ i $ j) 

我可以計算轉置矩陣：

(transpose (χ i j. if j = k then c * (A $ i $ j) else A $ i $ j)) 

在我眼裏後者應相當於

(χ i j. if i = k then c * (A $ j $ i) else A $ j $ i)) 

定義爲transpose。但是這是錯誤的。這裏有什麼錯誤？

順便說一句，換位的定義是：

definition transpose where 
    "(transpose::'a^'n^'m ⇒ 'a^'m^'n) A = (χ i j. ((A$j)$i))" 

Answer 1

我不知道你所說的意思：但事實卻並非如此。您預計什麼是真實，可以在伊莎貝爾如下證明：

lemma "transpose (χ i j. if j = k then c * (A $ i $ j) else A $ i $ j) = 
    (χ i j. if i = k then c * (A $ j $ i) else A $ j $ i)" 
    by (simp add: transpose_def)