Embedded Lattice and Properties of Gram Matrix

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.Search in Google Scholar

[2] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543-547, 1990.Search in Google Scholar

[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.Search in Google Scholar

[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.Search in Google Scholar

[5] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.Search in Google Scholar

[6] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.Search in Google Scholar

[7] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.Search in Google Scholar

[8] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.Search in Google Scholar

[9] Yuichi Futa and Yasunari Shidama. Lattice of Z-module. Formalized Mathematics, 24 (1):49-68, 2016. doi: 10.1515/forma-2016-0005.10.1515/forma-2016-0005Search in Google Scholar

[10] Yuichi Futa and Yasunari Shidama. Divisible Z-modules. Formalized Mathematics, 24 (1):37-47, 2016. doi: 10.1515/forma-2016-0004.10.1515/forma-2016-0004Search in Google Scholar

[11] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Z-modules. Formalized Mathe matics, 20(1):47-59, 2012. doi: 10.2478/v10037-012-0007-z.10.2478/v10037-012-0007-zSearch in Google Scholar

[12] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Quotient module of Z-module. Formalized Mathematics, 20(3):205-214, 2012. doi: 10.2478/v10037-012-0024-y.10.2478/v10037-012-0024-ySearch in Google Scholar

[13] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Matrix of Z-module. Formalized Mathematics, 23(1):29-49, 2015. doi: 10.2478/forma-2015-0003.10.2478/forma-2015-0003Search in Google Scholar

[14] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. doi: 10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1Search in Google Scholar

[15] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.Search in Google Scholar

[16] A. K. Lenstra, H. W. Lenstra Jr., and L. Lov´asz. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515-534, 1982. doi: 10.1007/BF01457454.10.1007/BF01457454Search in Google Scholar

[17] Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.10.1007/978-1-4615-0897-7_8Search in Google Scholar

[18] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3-11, 1991.Search in Google Scholar

[19] Karol Pak. Basic properties of the rank of matrices over a field. Formalized Mathematics, 15(4):199-211, 2007. doi: 10.2478/v10037-007-0024-5.10.2478/v10037-007-0024-5Search in Google Scholar

[20] Karol Pak and Andrzej Trybulec. Laplace expansion. Formalized Mathematics, 15(3): 143-150, 2007. doi: 10.2478/v10037-007-0016-5.10.2478/v10037-007-0016-5Search in Google Scholar

[21] 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.10.2478/v10037-007-0014-7Search in Google Scholar

[22] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990.Search in Google Scholar

[23] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990.Search in Google Scholar

[24] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.Search in Google Scholar

[25] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865-870, 1990.Search in Google Scholar

[26] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877-882, 1990.Search in Google Scholar

[27] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883-885, 1990.Search in Google Scholar

[28] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.Search in Google Scholar

[29] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.Search in Google Scholar