Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smul_ne_zero_iff

Modification history

2022-09-25 11:24

src/algebra/module/basic.lean

feat(algebra/module/basic): More general `smul_ne_zero` (#16608) …

Added smul_ne_zero_iff View on Github →