Product of torsion-free modules #
This file shows that the product of torsion-free modules is torsion-free.
instance
Pi.instModuleIsTorsionFree
{ι : Type u_1}
{R : Type u_2}
{M : ι → Type u_3}
[Semiring R]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.IsTorsionFree R (M i)]
:
Module.IsTorsionFree R ((i : ι) → M i)