mathlib

42f7ca0f - chore(linear_algebra/linear_independent): use `is_empty ι` instead of `¬nonempty ι` (#8331)