Product of torsion-free modules

This file shows that the product of two torsion-free modules is torsion-free.

instance Prod.moduleIsTorsionFree {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.IsTorsionFree R M] [Module.IsTorsionFree R N] : Module.IsTorsionFree R (M × N)