feat(linear_algebra/matrix): matrix has finite dim (#3013)
Using the fact that currying is a linear operation, we give matrix
a finite dimensional instance. This allows one to invoke `findim`
on matrices, giving the expected dimensions for a finite-dim matrix.
The import is changed to linear_algebra.finite_dimension,
which brings in the previous linear_algebra.dimension import.
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
