mathlib3

cc9d3ab1 - feat(algebra/module,linear_algebra): generalize `smul_eq_zero` (#6199)

feat(algebra/module,linear_algebra): generalize `smul_eq_zero` (#6199) Moves the theorem on division rings `smul_eq_zero` to a typeclass `no_zero_smul_divisors` with instances for the previously existing cases. The motivation for this change is that #6178 added another `smul_eq_zero`, which could be captured neatly as an instance of the typeclass. I didn't spend a lot of time yet on figuring out all the necessary instances, first let's see whether this compiles. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>