Embedded Lattice and Properties of Gram Matrix
In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2017-03-01
|
| Series: | Formalized Mathematics |
| Subjects: | |
| Online Access: | https://doi.org/10.1515/forma-2017-0007 |