Ein Teilformensatz für quadratische Formen in Charakteristik 2.
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-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].
Among normal linear spaces, the inner product spaces (i.p.s.) are particularly interesting. Many characterizations of i.p.s. among linear spaces are known using various functional equations. Three functional equations characterizations of i.p.s. are based on the Frchet condition, the Jordan and von Neumann identity and the Ptolemaic inequality respectively. The object of this paper is to solve generalizations of these functional equations.