no goals
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_1
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.88589
inst✝ : CommRing P
x : R
⊢ coeSubmodule S (Ideal.span {x}) = Submodule.span R {↑(algebraMap R S) x}
rw [coeSubmodule_span, Set.image_singleton]