Je n'ai pas trouvé la définition ou le lemme pour transposer un vecteur de type (real,'n) vec en théorie Finite_Cartesian_Product. J'essaie de substituer un vecteur transposé par une matrice de transposition et un vecteur, par exemple, si le vecteur e = A x puis la transposition de e (e^T) conduit à transposer A et x (e^T = A^T x^T). Puis-je faire ça chez Isabelle/HOL?Transposition de vecteur dans Isabelle/HOL
Tout d'abord, à moins que mon algèbre linéaire me manque complètement en ce moment, (AB)^T = B^T A^T, pas A^T B^T, de sorte que votre deuxième équation doit être e^T = x^T A^T
Pour répondre à votre question réelle: Je vous suggère de jeter un regard sur les constantes rowvector, columnvector et transpose de ~~/src/HOL/Analysis/Cartesian_Euclidean_Space. Les deux premiers vous permettent de transformer un vecteur de longueur n en une matrice 1 × n (respectivement n × 1) et cette dernière vous permet de transposer une matrice.
je suppose que votre e = A x ressemblerait columnvector e = A ** columnvector x et votre e^T = x^T A^T serait rowvector e = rowvector x ** transpose A.