R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.64270
inst✝ : CommRing P
s : Set R
⊢ Submodule.span R (↑(Algebra.linearMap R S) '' s) = Submodule.span R (↑(algebraMap R S) '' s)
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.64270
inst✝ : CommRing P
s : Set R
⊢ coeSubmodule S (Ideal.span s) = Submodule.span R (↑(algebraMap R S) '' s)
rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]
no goals
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.64270
inst✝ : CommRing P
s : Set R
⊢ Submodule.span R (↑(Algebra.linearMap R S) '' s) = Submodule.span R (↑(algebraMap R S) '' s)
rfl