Commit 2021-06-05 09:09 7021ff9b

feat(linear_algebra/basis): use is_empty instead of ¬nonempty (#7815) This removes the need for basis.of_dim_eq_zero' and basis_of_finrank_zero', as these special cases are now covered by the unprimed versions and typeclass search.