R : Type u_2
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_1
M'' : Type ?u.826565
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
m : M
⊢ ↑(fromLocalizedModule S f) (LocalizedModule.mk m 1) = ↑f m
R : Type u_2
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_1
M'' : Type ?u.826565
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
m : M
⊢ mk' f m 1 = ↑f m
delta mk'
no goals
R : Type u_2
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_3
M' : Type u_1
M'' : Type ?u.826565
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
m : M
⊢ ↑(fromLocalizedModule S f) (LocalizedModule.mk m 1) = ↑f m
rw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one,
  one_smul]