search

SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
16 stars 2 forks source link

Vector spaces and modules #33

Open SKolodynski opened 5 months ago

SKolodynski commented 5 months ago

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 commented 3 months ago

This has been done in 1.29.0.

dan323 commented 3 months ago

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 commented 3 months ago

Great, thanks.

dan323 commented 2 months ago

@SKolodynski review #35