R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_4
N : Type u_2
P : Type u_3
Q : Type ?u.1461678
S : Type ?u.1461681
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
f : N →ₗ[R] P
⊢ ↑(lTensorHom M) (-f) = -↑(lTensorHom M) f
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_4
N : Type u_2
P : Type u_3
Q : Type ?u.1461678
S : Type ?u.1461681
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
f : N →ₗ[R] P
⊢ lTensor M (-f) = -lTensor M f
simp only [← coe_lTensorHom]
no goals
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_4
N : Type u_2
P : Type u_3
Q : Type ?u.1461678
S : Type ?u.1461681
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup Q
inst✝⁵ : AddCommGroup S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R Q
inst✝ : Module R S
f : N →ₗ[R] P
⊢ ↑(lTensorHom M) (-f) = -↑(lTensorHom M) f
exact (lTensorHom (R:=R) (N:=N) (P:=P) M).map_neg f