no goals
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
S : Ideal R
inst✝ : IsPrincipal S
x a : R
⊢ x = a • generator S ↔ x = generator S * a
simp only [mul_comm, smul_eq_mul]