| 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} $ |
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