R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
h : IsTorsionBy R M a
x : M
⊢ ∀ ⦃a_1 : ↑{a}⦄, ↑a_1 • x = 0
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ IsTorsionBySet R M {a} ↔ IsTorsionBy R M a
refine' ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => _⟩
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
b : R
h : IsTorsionBy R M b
⊢ ↑{ val := b, property := (_ : b = b) } • x = 0
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
h : IsTorsionBy R M a
x : M
⊢ ∀ ⦃a_1 : ↑{a}⦄, ↑a_1 • x = 0
rintro ⟨b, rfl : b = a⟩
no goals
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
b : R
h : IsTorsionBy R M b
⊢ ↑{ val := b, property := (_ : b = b) } • x = 0
exact @h _