mathlib

7021ff9b - feat(linear_algebra/basis): use is_empty instead of ¬nonempty (#7815)

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.