R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
⊢ generator S ∈ span R {generator S}
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
⊢ generator S ∈ S
conv_rhs => rw [← span_singleton_generator S]
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
⊢ generator S ∈ span R {generator S}
exact subset_span (mem_singleton _)