R : Type u_3
inst✝¹² : CommRing R
S : Submonoid R
M✝ : Type ?u.858600
M'✝ : Type ?u.858603
M'' : Type ?u.858606
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 : Type u_1
M' : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : { x // x ∈ S }
⊢ ↑(fromLocalizedModule S f) (LocalizedModule.mk (-m) s) = -↑(fromLocalizedModule S f) (LocalizedModule.mk m s)
R : Type u_3
inst✝¹² : CommRing R
S : Submonoid R
M✝ : Type ?u.858600
M'✝ : Type ?u.858603
M'' : Type ?u.858606
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 : Type u_1
M' : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : { x // x ∈ S }
⊢ mk' f (-m) s = -mk' f m s
delta mk'
no goals
R : Type u_3
inst✝¹² : CommRing R
S : Submonoid R
M✝ : Type ?u.858600
M'✝ : Type ?u.858603
M'' : Type ?u.858606
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 : Type u_1
M' : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : { x // x ∈ S }
⊢ ↑(fromLocalizedModule S f) (LocalizedModule.mk (-m) s) = -↑(fromLocalizedModule S f) (LocalizedModule.mk m s)
rw [LocalizedModule.mk_neg, map_neg]