Isomorphism Theorem on Vector Spaces over a Ring

• Autorzy: Yuichi Futa , Yasunari Shidama
• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

isomorphism theorem; vector space

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 15A04: Linear transformations, semilinear transformations
• 15A03: Vector spaces, linear dependence, rank

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2017
• Tom: 25
• Numer: 3
• Strony: 171-178

Daty

wydano

2017-10-01

otrzymano

2017-08-30

online

2017-12-19

Twórcy

autor

Yuichi Futa

• , ,

autor

Yasunari Shidama

• , ,

Identyfikatory

DOI

10.1515/forma-2017-0016