mathlib3

59628387 - refactor(linear_algebra): make `module.free` available inside `linear_algebra/dimension` (#18717)

refactor(linear_algebra): make `module.free` available inside `linear_algebra/dimension` (#18717) Many of the results here should generalize from `division_ring K` to `module.free K V`, though this PR doesn't bother itself with making them. This PR just flips around the imports and moves the lemmas that can't stay in the old home, and makes no attempt to actually make this generalization. This also removes some duplicates: * `lemma equiv_of_dim_eq_lift_dim` duplicates `nonempty_linear_equiv_of_lift_dim_eq` * `def equiv_of_dim_eq_dim` duplicates `linear_equiv.of_dim_eq` A few downstream files now need to directly import `linear_algebra.dimension`, which previously was implied transitively.