| context | X |
| context | n,k∈N |
| definition | ⋅ T:Matrix(n,k,X)→Matrix(k,n,X) |
| postulate | (AT)ij=Aji |
mm = {{a, b, c}, {x, y, z}};
tm = Transpose[mm];
mm // MatrixForm
tm // MatrixForm
--$ idris -p contrib --$ :l this_module.idr import Data.Matrix mm : Matrix 3 2 Nat mm = [[3,5],[1,5],[2,1]] tm : Matrix 2 3 Nat tm = transpose mm
Wikipedia: Transpose