theorem tensor_rTensor_rightExact {R : Type u_1} [CommRing R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (A : Type u_5) [AddCommGroup A] [Module R A] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) : Function.Exact ⇑(LinearMap.rTensor A f) ⇑(LinearMap.rTensor A g) ∧ Function.Surjective ⇑(LinearMap.rTensor A g)