Formalized Mathematics    ISSN 1898-9934 (e), ISSN 1426-2630 (p)

 Volume 16, Number 2 (2008): PDF A copy of this issue can also be found on the MetaPress server (with DOI names of articles).

1. Jessica Enright, Piotr Rudnicki. Helly Property for Subtrees, Formalized Mathematics 16(2), pages 91-96, 2008. MML Identifier: HELLY
Summary: We prove, following \cite[p.92]{Golumbic}, that any family of subtrees of a finite tree satisfies the Helly property.
2. Marco Riccardi. Heron's Formula and {P}tolemy's Theorem, Formalized Mathematics 16(2), pages 97-101, 2008. MML Identifier: EUCLID_6
Summary: The goal of this article is to formalize some theorems that are in the \cite{Freek-100-theorems} on the web. These are elementary theorems included in every handbook of Euclidean geometry and trigonometry: the law of cosines, the Heron's formula, the isosceles triangle theorem, the intersecting chords theorem and the Ptolemy's theorem.
3. Hiroyuki Okazaki, Yasunari Shidama. Uniqueness of Factoring an Integer and Multiplicative Group ${\mathbb Z}/p{{\mathbb Z}^\ast}$, Formalized Mathematics 16(2), pages 103-107, 2008. MML Identifier: INT_7
Summary: In the \cite{INT_3.ABS}, it had been proven that the Integers modulo $p$, in this article we shall refer as ${\mathbb Z}/p{\mathbb Z}$, constitutes a field if and only if $p$ is a prime. Then the prime modulo ${\mathbb Z}/p{\mathbb Z}$ is an additive cyclic group and ${\mathbb Z}/p{{\mathbb Z}^\ast}={\mathbb Z}/p{\mathbb Z}\setminus\{0\}$ is a multiplicative cyclic group, too. The former has been proven in the \cite{GR_CY_1.ABS}. However, the latter had not been proven yet. In this article, first, we prove a theorem concerning the LCM to prove the existence of primitive elements of ${\mathbb Z}/p^{\ast}$. Moreover we prove the uniqueness of factoring an integer. Next we define the multiplicative group ${\mathbb Z}/p{{\mathbb Z}^\ast}$ and prove it is cyclic.
4. Chenglong Wu, Yuzhong Ding. Ideals of {BCI}-algebras and their Properties, Formalized Mathematics 16(2), pages 109-114, 2008. MML Identifier: BCIIDEAL
Summary: In this article three classes of ideals are discussed: associative ideals, commutative ideals, implicative ideals and positive implicative ideals, and their elementary properties. Some of their properties and the relationships between them have not been proven yet, and will be completed in the following article.
5. Yasunari Shidama, Hikofumi Suzuki, Noboru Endou. Banach Algebra of Bounded Functionals, Formalized Mathematics 16(2), pages 115-122, 2008. MML Identifier: C0SP1
Summary: In this article, we describe some basic properties of the Banach algebra which is constructed from all bounded functionals.
6. Hidenori Matsuzaki, Noboru Endou, Yasunari Shidama. Convex Sets and Convex Combinations on Complex Linear Spaces, Formalized Mathematics 16(2), pages 123-133, 2008. MML Identifier: CONVEX4
Summary: In this article, convex sets, convex combinations and convex hulls on complex linear spaces are introduced.
7. Fuguo Ge. Inner Products, Group, Ring of Quaternion Numbers, Formalized Mathematics 16(2), pages 135-139, 2008. MML Identifier: QUATERN2
Summary: In this article, we define the division of the quaternion numbers, we also give the definition of inner products, group, ring of the quaternion numbers, and we prove some of their properties.
8. Junjie Zhao, Xiquan Liang, Li Yan. Several Higher Differentiation Formulas of Special Functions, Formalized Mathematics 16(2), pages 141-145, 2008. MML Identifier: HFDIFF_1
Summary: In this paper, we proved some basic properties of higher differentiation, and higher differentiation formulas of special functions \cite{Chen:1978}.
9. Xiquan Liang, Bing Xie. Inverse Trigonometric Functions Arctan and Arccot, Formalized Mathematics 16(2), pages 147-158, 2008. MML Identifier: SIN_COS9
Summary: This article describes definitions of inverse trigonometric functions arctan, arccot and their main properties, as well as several differentiation formulas of arctan and arccot.
10. Bing Xie, Xiquan Liang, Fuguo Ge. Inverse Trigonometric Functions Arcsec and Arccosec, Formalized Mathematics 16(2), pages 159-165, 2008. MML Identifier: SINCOS10
Summary: This article describes definitions of inverse trigonometric functions arcsec and arccosec, as well as their main properties.
11. Noboru Endou, Keiko Narita, Yasunari Shidama. The {L}ebesgue Monotone Convergence Theorem, Formalized Mathematics 16(2), pages 167-175, 2008. MML Identifier: MESFUNC9