%0 Journal Article
%T Formalization of Integral Linear Space
%A Yuichi Futa
%A Hiroyuki Okazaki
%A Yasunari Shidama
%J Formalized Mathematics
%@ 1898-9934
%D 2011
%I 
%R 10.2478/v10037-011-0010-9
%X In this article, we formalize integral linear spaces, that is a linear space with integer coefficients. Integral linear spaces are necessary for lattice problems, LLL (Lenstra-Lenstra-Lov¨¢sz) base reduction algorithm that outputs short lattice base and cryptographic systems with lattice [8].
%U http://versita.metapress.com/content/x38l056353582201/?p=25816f9e6d274cf5ab90abc2a2c39abd&pi=9