SKolodynski

Vector spaces and modules

4

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...

The dependency for this statement is to define the natural topology on the real numbers. This is probably best done through metric spaces. Since pseudometrics play a role in the...