DSpace Kolekcja:http://hdl.handle.net/11320/48012020-11-27T07:41:51Z2020-11-27T07:41:51ZConservation Rules of Direct Sum Decomposition of GroupsNakasho, KazuhisaYamazaki, HiroshiOkazaki, HiroyukiShidama, Yasunarihttp://hdl.handle.net/11320/54922017-10-05T23:13:34Z2016-01-01T00:00:00ZTytuł: Conservation Rules of Direct Sum Decomposition of Groups
Autorzy: Nakasho, Kazuhisa; Yamazaki, Hiroshi; Okazaki, Hiroyuki; Shidama, Yasunari
Abstrakt: In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.2016-01-01T00:00:00ZLattice of ℤ-moduleFuta, YuichiShidama, Yasunarihttp://hdl.handle.net/11320/54902017-10-05T23:13:31Z2016-01-01T00:00:00ZTytuł: Lattice of ℤ-module
Autorzy: Futa, Yuichi; Shidama, Yasunari
Abstrakt: In this article, we formalize the definition of lattice of ℤ-module and its properties in the Mizar system [5].We formally prove that scalar products in lattices are bilinear forms over the field of real numbers ℝ. We also formalize the definitions of positive definite and integral lattices and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [14], and cryptographic systems with lattices [15] and coding theory [9].2016-01-01T00:00:00ZProduct Pre-MeasureEndou, Noboruhttp://hdl.handle.net/11320/54912017-10-05T23:13:32Z2016-01-01T00:00:00ZTytuł: Product Pre-Measure
Autorzy: Endou, Noboru
Abstrakt: In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.2016-01-01T00:00:00ZAltitude, Orthocenter of a Triangle and TriangulationCoghetto, Rolandhttp://hdl.handle.net/11320/54882017-10-05T23:13:29Z2016-01-01T00:00:00ZTytuł: Altitude, Orthocenter of a Triangle and Triangulation
Autorzy: Coghetto, Roland
Abstrakt: We introduce the altitudes of a triangle (the cevians perpendicular to the opposite sides). Using the generalized Ceva’s Theorem, we prove the existence and uniqueness of the orthocenter of a triangle [7]. Finally, we formalize in Mizar [1] some formulas [2] to calculate distance using triangulation.2016-01-01T00:00:00Z