mathlib

bf2a9e01 - chore(linear_algebra): import `free_module.finite.rank` from `finite_dimensional` (#17482)

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`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>