theorem
tensor_rTensor_additive
{R : Type u_1}
[CommRing R]
{M : Type u_2}
{N : Type u_3}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
(A : Type u_4)
[AddCommGroup A]
[Module R A]
:
LinearMap.rTensor A 0 = 0 ∧ ∀ (f g : M →ₗ[R] N), LinearMap.rTensor A (f + g) = LinearMap.rTensor A f + LinearMap.rTensor A g