Vector spaces and modules

[SKolodynski]

I am working on adding definitions of modules and vector spaces. This will be defined as ring or field actions on abelian groups, with Ring_ZF_2 and Ring_ZF_3 as dependencies (hence recent changes to those so that they can be presented at isarmathlib.org).

[SKolodynski]

This has been done in 1.29.0.

[dan323]

I was working on that, so I will try to update to the definitons you added the extra results I achieved about linear dependency.

[SKolodynski]

Great, thanks.

[dan323]

@SKolodynski review #35