In this article, we formalize in the Mizar system [1, 4] some properties of vector spaces over a ring. We formally prove the first isomorphism theorem of vector spaces over a ring. We also formalize the product space of vector spaces. ℤ-modules are useful for lattice problems such as LLL (Lenstra, Lenstra and Lovász) [5] base reduction algorithm and cryptographic systems [6, 2].
@article{bwmeta1.element.doi-10_1515_forma-2017-0016,
author = {Yuichi Futa and Yasunari Shidama},
title = {Isomorphism Theorem on Vector Spaces over a Ring},
journal = {Formalized Mathematics},
volume = {25},
year = {2017},
pages = {171-178},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0016}
}
Yuichi Futa; Yasunari Shidama. Isomorphism Theorem on Vector Spaces over a Ring. Formalized Mathematics, Tome 25 (2017) pp. 171-178. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0016/