Commit 2023-04-03 10:26 59628387

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.