R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_2
M'' : Type ?u.808793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
r : R
m : M
s : { x // x ∈ S }
⊢ ↑(fromLocalizedModule S f) (LocalizedModule.mk (r • m) s) = r • ↑(fromLocalizedModule S f) (LocalizedModule.mk m s)
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_2
M'' : Type ?u.808793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
r : R
m : M
s : { x // x ∈ S }
⊢ mk' f (r • m) s = r • mk' f m s
delta mk'
no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_2
M'' : Type ?u.808793
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
r : R
m : M
s : { x // x ∈ S }
⊢ ↑(fromLocalizedModule S f) (LocalizedModule.mk (r • m) s) = r • ↑(fromLocalizedModule S f) (LocalizedModule.mk m s)
rw [← LocalizedModule.smul'_mk, LinearMap.map_smul]