search

SKolodynski / IsarMathLib

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

More on modules #36

Closed dan323 closed 2 months ago

dan323 commented 2 months ago

Module_ZF_2.thy

IntModule_ZF.thy

Every abelian group admits one, and only one, action from the integers.