| context | $X$ … set |
| context | $n,m\in \mathbb N$ |
| definiendum | $ A\in \mathrm{Matrix}(n,m,X) $ |
| postulate | $$ A\in\mathrm{FinSequence}(\mathrm{FinSequence}(X)) $$ |
| range | $ 1\ge i\ge m$ |
| postulate | $\mathrm{length}(A)=n$ |
| postulate | $\mathrm{length}(A_i)=m$ |
We write
$A_{ij}\equiv (A_i)_j$
Wikipedia: Matrix_(mathematics)
Mathematica: MatrixOperations
Idris: contrib/Data/Matrix.idr
Haskell: package/matrix-0.3.5.0/docs/Data-Matrix.html