Commit 2020-06-10 19:03 2779093b

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.