R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.645266
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
x : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.645266
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
x : LocalizedModule S M
⊢ ∀ (m : M) (s : { x // x ∈ S }),
    r • fromLocalizedModule' S f (LocalizedModule.mk m s) = fromLocalizedModule' S f (r • LocalizedModule.mk m s)
intro a b
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.645266
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
x : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M')) ↑b)))⁻¹ (↑f a) =
    ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M')) ↑b)))⁻¹ (↑f (r • a))
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.645266
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
x : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)
rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk]
no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type ?u.645266
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
x : LocalizedModule S M
a : M
b : { x // x ∈ S }
⊢ r • ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M')) ↑b)))⁻¹ (↑f a) =
    ↑↑(IsUnit.unit (_ : IsUnit (↑(algebraMap R (Module.End R M')) ↑b)))⁻¹ (↑f (r • a))
rw [f.map_smul, map_smul]