×

Matrix of \(\mathbb{Z}\)-module. (English) Zbl 1317.11037

Summary: In this article, we formalize a matrix of \(\mathbb{Z}\)-module and its properties. Specially, we formalize a matrix of a linear transformation of \(\mathbb{Z}\)-module, a bilinear form and a matrix of the bilinear form (Gramian matrix). We formally prove that for a finite-rank free \(\mathbb{Z}\)-module \(V\), determinant of its Gramian matrix is constant regardless of selection of its basis. \(\mathbb{Z}\)-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattices [D. Micciancio and S. Goldwasser, Complexity of lattice problems. A cryptographic perspective. Boston, MA: Kluwer Academic Publishers (2002; Zbl 1140.94010)] and coding theory [W. Ebeling, Lattices and codes. A course partially based on lectures by Friedrich Hirzebruch. 3rd revised ed. Berlin: Springer (2013; Zbl 1257.11066)]. Some theorems in this article are described by translating theorems in [R. Milewski, “Associated matrix of linear map”, Formaliz. Math. 5, No. 3, 339–345 (1996); B. Nowak and A. Trybulec, “Hahn-Banach theorem”, Formaliz. Math. 4, No. 1, 29–34 (1993); J. Kotowicz, “Bilinear functionals in vector spaces”, Formaliz. Math. 11, No. 1, 69–86 (2003)] into theorems of \(\mathbb{Z}\)-module.

MSC:

11E39 Bilinear and Hermitian forms
13C10 Projective and free modules and ideals in commutative rings
03B35 Mechanization of proofs and logical operations
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.;
[2] Grzegorz Bancerek. Curried and uncurried functions. Formalized Mathematics, 1(3): 537-541, 1990.;
[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.; · Zbl 1364.68157
[4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.;
[5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.;
[6] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.;
[7] Czesław Byliński. Binary operations applied to finite sequences. Formalized Mathematics, 1(4):643-649, 1990.;
[8] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.;
[9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.;
[10] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.;
[11] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.;
[12] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.;
[13] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.;
[14] Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013.; · Zbl 1257.11066
[15] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. ℤ-modules. Formalized Mathematics, 20(1):47-59, 2012. doi:10.2478/v10037-012-0007-z.; · Zbl 1276.94012
[16] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Free ℤ-module. Formalized Mathematics, 20(4):275-280, 2012. doi:10.2478/v10037-012-0033-x.; · Zbl 1364.13010
[17] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2 (4):475-480, 1991.;
[18] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990.;
[19] Jarosław Kotowicz. Bilinear functionals in vector spaces. Formalized Mathematics, 11(1): 69-86, 2003.;
[20] Jarosław Kotowicz. Partial functions from a domain to a domain. Formalized Mathematics, 1(4):697-702, 1990.;
[21] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.;
[22] Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.; · Zbl 1140.94010
[23] Anna Justyna Milewska. The Hahn Banach theorem in the vector space over the field of complex numbers. Formalized Mathematics, 9(2):363-371, 2001.;
[24] Robert Milewski. Associated matrix of linear map. Formalized Mathematics, 5(3):339-345, 1996.;
[25] Michał Muzalewski. Rings and modules - part II. Formalized Mathematics, 2(4):579-585, 1991.;
[26] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Formalized Mathematics, 4(1):29-34, 1993.;
[27] Karol Pąk and Andrzej Trybulec. Laplace expansion. Formalized Mathematics, 15(3): 143-150, 2007. doi:10.2478/v10037-007-0016-5.;
[28] Christoph Schwarzweller. The ring of integers, Euclidean rings and modulo integers. Formalized Mathematics, 8(1):29-34, 1999.;
[29] Nobuyuki Tamura and Yatsuka Nakamura. Determinant and inverse of matrices of real elements. Formalized Mathematics, 15(3):127-136, 2007. doi:10.2478/v10037-007-0014-7.;
[30] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990.;
[31] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.;
[32] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990.;
[33] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575-579, 1990.;
[34] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990.;
[35] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.;
[36] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1(5):877-882, 1990.;
[37] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883-885, 1990.;
[38] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.;
[39] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.;
[40] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.;
[41] Katarzyna Zawadzka. The sum and product of finite sequences of elements of a field. Formalized Mathematics, 3(2):205-211, 1992.;
[42] Katarzyna Zawadzka. The product and the determinant of matrices with entries in a field. Formalized Mathematics, 4(1):1-8, 1993.;
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.