mathlib

d6fd5f5f - feat(linear_algebra/dimension): generalize dim_zero_iff_forall_zero (#9713)

feat(linear_algebra/dimension): generalize dim_zero_iff_forall_zero (#9713) We generalize `dim_zero_iff_forall_zero` to `[nontrivial R] [no_zero_smul_divisors R M]`. If you see a more general class to consider let me know.