R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x✝ : M
h : x✝ ∈ torsionBy R M 1
⊢ x✝ ∈ ⊥
rw [mem_torsionBy_iff, one_smul] at h
no goals
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥
exact h