no goals
R : Type u
M : Type v
F : Type ?u.187576
G : Type ?u.187579
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N✝ N₁ N₂ P P₁ P₂ N : Submodule R M
x : M
r : R
⊢ r ∈ colon N (span R {x}) ↔ ∀ (a : R), r • a • x ∈ N
simp [Submodule.mem_colon, Submodule.mem_span_singleton]
R : Type u
M : Type v
F : Type ?u.187576
G : Type ?u.187579
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N✝ N₁ N₂ P P₁ P₂ N : Submodule R M
x : M
r : R
⊢ (∀ (a : R), a • r • x ∈ N) ↔ r • x ∈ N
R : Type u
M : Type v
F : Type ?u.187576
G : Type ?u.187579
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N✝ N₁ N₂ P P₁ P₂ N : Submodule R M
x : M
r : R
⊢ (∀ (a : R), r • a • x ∈ N) ↔ r • x ∈ N
simp_rw [fun (a : R) ↦ smul_comm r a x]
no goals
R : Type u
M : Type v
F : Type ?u.187576
G : Type ?u.187579
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N✝ N₁ N₂ P P₁ P₂ N : Submodule R M
x : M
r : R
⊢ (∀ (a : R), a • r • x ∈ N) ↔ r • x ∈ N
exact SetLike.forall_smul_mem_iff