refactor(linear_algebra/basic): split file (#12637)

`linear_algebra.basic` has become a 2800 line monster, with lots of imports.

This is some further work on splitting it into smaller pieces, by extracting everything about (or needing) `span` to `linear_algebra.span`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/algebra/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import algebra.module.basic
-import linear_algebra.basic
+import linear_algebra.span
 import tactic.abel
 import data.equiv.ring_aut
 

src/algebra/module/submodule_pointwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import group_theory.subgroup.pointwise
-import linear_algebra.basic
+import linear_algebra.span
 
 /-! # Pointwise instances on `submodule`s
 

src/analysis/normed_space/finite_dimension.lean

@@ -684,7 +684,7 @@ let ⟨g, hg⟩ := (f : E →ₗ[𝕜] F).exists_right_inverse_of_surjective hf
 ⟨g.to_continuous_linear_map, continuous_linear_map.ext $ linear_map.ext_iff.1 hg⟩
 
 lemma closed_embedding_smul_left {c : E} (hc : c ≠ 0) : closed_embedding (λ x : 𝕜, x • c) :=
-linear_equiv.closed_embedding_of_injective (linear_equiv.ker_to_span_singleton 𝕜 E hc)
+linear_equiv.closed_embedding_of_injective (linear_map.ker_to_span_singleton 𝕜 E hc)
 
 /- `smul` is a closed map in the first argument. -/
 lemma is_closed_map_smul_left (c : E) : is_closed_map (λ x : 𝕜, x • c) :=