×

Formalization of integral linear space. (English) Zbl 1276.15001

Summary: 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.

MSC:

15A03 Vector spaces, linear dependence, rank, lineability
94A60 Cryptography
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. · Zbl 1364.68157
[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
[4] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
[5] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Dimension of real unitary space. Formalized Mathematics, 11(1):23-28, 2003.
[6] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990.
[7] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990.
[8] Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: A cryptographic perspective (the international series in engineering and computer science). 2002. · Zbl 1140.94010
[9] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329-334, 1990.
[10] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990.
[11] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
[12] Wojciech A. Trybulec. Basis of real linear space. Formalized Mathematics, 1(5):847-850, 1990.
[13] Wojciech A. Trybulec. Linear combinations in real linear space. Formalized Mathematics, 1(3):581-588, 1990.
[14] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
[15] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
[16] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.
[17] Hiroshi Yamazaki and Yasunari Shidama. Algebra of vector functions. Formalized Mathematics, 3(2):171-175, 1992.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.