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

Question

矩阵的* 和** 有什么区别 还有 A * 1andA ** mat 1`?

例子：

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 中的矩阵被简单地定义为向量的向量，因此矩阵上的* 是从向量继承的，而向量上的* 只是按分量相乘。因此，您有(A*B) $ i $ j = A $ i $ j * B $ i $ j，即* 是矩阵的逐项乘法。这在任何地方是否真的有用，我不知道——我不这么认为。它可能只是将矩阵定义为向量的向量的产物。为矩阵做一个适当的 typedef 并将 * 定义为它们的 right 矩阵乘法可能会更好，但一定有一些原因导致没有这样做——也许只是因为它更多工作和大量复制粘贴的代码。

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

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