mathlib3
585d6419 - refactor(linear_algebra/basic): split file (#12637)

Commit
3 years ago
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>
Author
Parents
Loading