mathlib

3b727dc2 - feat(algebra/module/basic): More general `smul_ne_zero` (#16608)

feat(algebra/module/basic): More general `smul_ne_zero` (#16608) Prove the one way implication of `smul_ne_zero` that holds without `smul_eq_zero` separately. Call it `smul_ne_zero` and rename `smul_ne_zero` to `smul_ne_zero_iff`. This matches `mul_ne_zero` and `mul_ne_zero_iff`.