Commit 2023-04-09 07:51 b1c23399

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.