Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smul_ne_zero

Modification history

2022-09-25 11:24
src/algebra/module/basic.lean
feat(algebra/module/basic): More general `smul_ne_zero` (#16608) …
Modified smul_ne_zeroView on Github →
2021-03-07 14:37
src/algebra/module/basic.lean
fead(data/support): add `support_smul` (#6569) …
Added smul_ne_zeroView on Github →