Quotient Module of Z-module

In this article we formalize a quotient module of Z-module and a vector space constructed by the quotient module. We formally prove that for a Z-module V and a prime number p, a quotient module V/pV has the structure of a vector space over Fp. Z-module is necessary for lattice problems, LLL (Lenstra...

Full description

Bibliographic Details
Main Authors: Futa Yuichi, Okazaki Hiroyuki, Shidama Yasunari
Format: Article
Language:English
Published: Sciendo 2012-12-01
Series:Formalized Mathematics
Online Access:https://doi.org/10.2478/v10037-012-0024-y