Commit 2021-02-22 18:48 cc9d3ab1

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.