Tensor products of projective modules

The tensor product of projective modules is projective.

instance Module.Projective.tensorProduct {R : Type u_1} [Semiring R] {R₀ : Type u_3} {M : Type u_2} {N : Type u_4} [CommSemiring R₀] [Algebra R₀ R] [AddCommMonoid M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [AddCommMonoid N] [Module R₀ N] [hM : Projective R M] [hN : Projective R₀ N] : Projective R (TensorProduct R₀ M N)