α : Type ?u.276095
R : Type ?u.276098
k : Type ?u.276101
S : Type ?u.276104
M : Type u_1
M₂ : Type ?u.276110
M₃ : Type ?u.276113
ι : Type ?u.276116
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
this : NoZeroSMulDivisors ℕ M
⊢ 2 • v = 0 ↔ v = 0
α : Type ?u.276095
R : Type ?u.276098
k : Type ?u.276101
S : Type ?u.276104
M : Type u_1
M₂ : Type ?u.276110
M₃ : Type ?u.276113
ι : Type ?u.276116
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
⊢ 2 • v = 0 ↔ v = 0
haveI := Nat.noZeroSMulDivisors R M
no goals
α : Type ?u.276095
R : Type ?u.276098
k : Type ?u.276101
S : Type ?u.276104
M : Type u_1
M₂ : Type ?u.276110
M₃ : Type ?u.276113
ι : Type ?u.276116
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
this : NoZeroSMulDivisors ℕ M
⊢ 2 • v = 0 ↔ v = 0
simp [smul_eq_zero]