mathlib

b1c23399 - refactor(linear_algebra/matrix/finite_dimensional): deduplicate (#18770)

refactor(linear_algebra/matrix/finite_dimensional): deduplicate (#18770) * `matrix.finrank_matrix` was a duplicate of `finite_dimensional.finrank_matrix`. * `linear_map.finrank_linear_map` was a duplicate of `finrank_linear_hom`, now merged to `finite_dimensional.finrank_linear_map` * `finite_dimensional.linear_map` was a duplicate of `linear_map.finite_dimensional` and can be golfed using `module.finite.linear_map` * `finite_dimensional.matrix` can be golfed using `module.finite.matrix` For now, I've left behind `finite_dimensional` instances, but proved them in terms of the `module.finite` versions. To enable this, some imports have been adjusted. The resulting import structure substantially cuts the dependencies consumed by `linear_algebra.matrix.to_lin`; it no longer needs `module.rank` to be available. Co-authored-by: Jeremy Tan Jie Rui <e0191785@u.nus.edu>