Commit 2022-02-10 20:44 fb41da97

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