mathlib3

21271659 - chore(linear_algebra/basis): split off `linear_independent.lean` (#4440)

chore(linear_algebra/basis): split off `linear_independent.lean` (#4440) The file `basis.lean` was getting rather long (1500 lines), so I decided to split it into two not as long files at a natural point: everything using `linear_independent` but not `basis` can go into a new file `linear_independent.lean`. As a result, we can import `basis.lean` a bit later in the `ring_theory` hierarchy.