Commit 2020-10-05 19:45 21271659

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.