Commit 2022-09-25 11:24 3b727dc2
View on Github →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.