R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ torsionBySet R M Set.univ ≤ torsionBySet R M {1}
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ torsionBySet R M Set.univ = ⊥
rw [eq_bot_iff, ← torsionBy_one, ← torsionBySet_singleton_eq]
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
⊢ torsionBySet R M Set.univ ≤ torsionBySet R M {1}
exact torsionBySet_le_torsionBySet_of_subset fun _ _ => trivial