Define free R-module as tensor product of R and free abelian group

[Alizter]

We should develop the theory of the free R-module on a set X by defining it as the tensor product of R and the free abelian group on X and showing standard properties like functoriality as we have done for the free abelian group.

It should either go in Module.v or in its own file FreeModule.v.

There is some choice whether to choose a left or right module, but a left module makes more sense with R being tensored on the right.