私のイザベル理論では、定数係数を持つ行列があります。
...
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))"