Skip to content

Commit

Permalink
chore(linear_algebra/basis): split off linear_independent.lean (#4440)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@Vierkantor
Vierkantor committed Oct 5, 2020
1 parent 88c76ab commit 2127165
Show file tree
Hide file tree
Showing 4 changed files with 935 additions and 876 deletions.

0 comments on commit 2127165

Please sign in to comment.