no goals
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
⊢ S = ⊥ ↔ generator S = 0
rw [← @span_singleton_eq_bot R M, span_singleton_generator]