isabelle - 伊莎贝尔：A * 1 和 A ** mat 1 的区别

Question

矩阵和 A * 1 *A ** mat 1`之间有什么区别？**and

例子：

lemma myexample:
  fixes A :: "('a::comm_ring_1)^'n∷finite^'n∷finite"
  shows "(A * 1 = A) ∧ (A ** (mat 1) = A)" 
 by (metis comm_semiring_1_class.normalizing_semiring_rules(12) matrix_mul_rid)

Answer 1

Isabelle 中的矩阵被简单地定义为向量的向量，因此*on 矩阵是从向量继承的，而*on 向量只是按分量相乘。因此，您有(A*B) $ i $ j = A $ i $ j * B $ i $ j, 即*是矩阵的逐项乘法。这在任何地方是否真的有用，我不知道——我不这么认为。它可能只是将矩阵定义为向量的向量的产物。*对矩阵进行适当的 typedef 并将其定义为正确的矩阵乘法可能会更好，但一定有一些原因为什么没有这样做 - 也许只是因为它需要更多的工作和大量的复制粘贴代码。

**是正确的矩阵乘法。mat x只是在x对角线上和0其他任何地方都有的矩阵，所以当然mat 1是单位矩阵和A ** mat 1 = A。

然而，矩阵1再次是来自向量定义的伪影；n 维向量1被简单地定义为具有 n 个分量的向量，所有分量都是1。因此，矩阵1是其条目全部为 的矩阵1，然后当然是A * 1 = A。这对我来说似乎没有任何用处。