Commit 2022-11-15 22:05 bf2a9e01

chore(linear_algebra): import free_module.finite.rank from finite_dimensional (#17482) This PR reworks the import structure between linear_algebra.free_module.finite and linear_algebra.finite_dimensional with the goal of reducing the length of the dependency chain, and importing linear_algebra.free_module.finite.rank from linear_algebra.finite_dimensional instead of vice versa. In addition to the changes in #17473 and #17474, this PR removes the import of linear_algebra.matrix.to_lin from linear_algebra.free_module.finite.basic, moving the dependent lemmas to linear_algebra.free_module.finite.matrix.