This is an old revision of the document!
Matrix transpose
Function
context | $X$ |
context | $n,k\in\mathbb N$ |
definition | ${\cdot}^{\ \mathrm{T}}: \mathrm{Matrix}(n,k,X) \to \mathrm{Matrix}(k,n,X) $ |
postulate | $(A^\mathrm{T})_{ij}=A_{ji} $ |
Discussion
Code
M = {{a, b, c}, {x, y, z}}; TM = Transpose[M]; M // MatrixForm TM // MatrixForm
--$ idris -p contrib --$ :l this_module.idr import Data.Matrix m : Matrix 3 2 Nat m = [[3,5],[1,5],[2,1]] tm : Matrix 2 3 Nat tm = transpose m
Reference
Wikipedia: Transpose