【发布时间】：2017-05-26 17:19:04
【问题描述】：
我找不到在Finite_Cartesian_Product 理论中转置(real,'n) vec 类型向量的定义或引理。我正在尝试用转置矩阵和向量替换转置向量，例如，如果向量e = A x 的转置e(e^T) 导致转置A 和x (@ 987654328@)。我可以在 Isabelle/HOL 中执行此操作吗？
【问题讨论】：
标签： isabelle
【发布时间】：2017-05-26 17:19:04
【问题描述】：
首先，除非我的线性代数现在完全失败了，(AB)^T = B^T A^T，而不是A^T B^T，所以你的第二个方程应该是e^T = x^T A^T
要回答您的实际问题：我建议您查看来自~~/src/HOL/Analysis/Cartesian_Euclidean_Space 的常量rowvector、columnvector 和transpose。前两个允许您将长度为n 的向量转换为1 × n（分别为n × 1）矩阵，后者允许您转置矩阵。
我猜你的e = A x 看起来像columnvector e = A ** columnvector x 而你的e^T = x^T A^T 应该是rowvector e = rowvector x ** transpose A。
【讨论】：