Formalization of Integral Linear Space
Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama · Formalized Mathematics · 2011
Formalization of Integral Linear SpaceIn 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].