no goals
α : Type ?u.267693
R : Type u_2
k : Type ?u.267699
S : Type ?u.267702
M : Type u_1
M₂ : Type ?u.267708
M₃ : Type ?u.267711
ι : Type ?u.267714
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
⊢ c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0
rw [Ne.def, smul_eq_zero, not_or]