mathlib

fb41da97 - feat(algebra/module/basic): turn implications into iffs (#11937)

feat(algebra/module/basic): turn implications into iffs (#11937) * Turn the following implications into `iff`, rename them accordingly, and make the type arguments explicit (`M` has to be explicit when using it in `rw`, otherwise one will have unsolved type-class arguments) ``` eq_zero_of_two_nsmul_eq_zero -> two_nsmul_eq_zero eq_zero_of_eq_neg -> self_eq_neg ne_neg_of_ne_zero -> self_ne_neg ``` * Also add two variants * Generalize `ne_neg_iff_ne_zero` to work in modules over a ring