mathlib3
6c263e4b - chore(linear_algebra/matrix/basis): reduce imports (#18823)

Commit
2 years ago
chore(linear_algebra/matrix/basis): reduce imports (#18823) This is a slight simplification on the current maximal path for the port. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading