no goals
R : Type u
M : Type v
F : Type ?u.199912
G : Type ?u.199915
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N N₁ N₂ P P₁ P₂ : Submodule R M
I : Ideal R
x r : R
⊢ r ∈ colon I (Ideal.span {x}) ↔ r * x ∈ I
simp only [← Ideal.submodule_span_eq, Submodule.mem_colon_singleton, smul_eq_mul]