no goals
R : Type u
M : Type v
F : Type ?u.20043
G : Type ?u.20046
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I J : Ideal R
N P : Submodule R M
g : M
r : R
⊢ r ∈ annihilator (span R {g}) ↔ r • g = 0
simp [mem_annihilator_span]