In this paper we formalized some theorems concerning the cyclic groups of prime power order. We formalize that every commutative cyclic group of prime power order is isomorphic to a direct product of family of cyclic groups [1], [18].
We have been working on the formalization of groups. In [1], we encoded some theorems concerning the product of cyclic groups. In this article, we present the generalized formalization of [1]. First, we show that every finite commutative group which order is composite number is isomorphic to a direct product of finite commutative groups which orders are relatively prime. Next, we describe finite direct products of finite commutative groups
In this article, we formalize that every finite cyclic group is isomorphic to a direct product of finite cyclic groups which orders are relative prime. This theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups and the fundamental theorem of finite abelian groups. Moreover, we formalize some facts about the product of a finite sequence of abelian groups.
In the paper the invariant (geometrical) character of some properties of natural planar ternary rings is shown by using isotopic transformations.
According to S. Krstić, there are only four quadratic varieties which are closed under isotopy. We give a simple procedure generating quadratic identities and deciding which of the four varieties they define. There are about 37000 such identities with up to five variables.
In this paper we apply techniques of spherical harmonic analysis to prove a local limit theorem, a rate of escape theorem, and a central limit theorem for isotropic random walks on arbitrary thick regular affine buildings of irreducible type. This generalises results of Cartwright and Woess where buildings are studied, Lindlbauer and Voit where buildings are studied, and Sawyer where homogeneous trees are studied (these are buildings).
If is an isotype knice subgroup of a global Warfield group , we introduce the notion of a -subgroup to obtain various necessary and sufficient conditions on the quotient group in order for itself to be a global Warfield group. Our main theorem is that is a global Warfield group if and only if possesses an -family of almost strongly separable -subgroups. By an -family we mean an Axiom 3 family in the strong sense of P. Hill. As a corollary to the main theorem, we are able to characterize...
In this paper, we initiate the study of various classes of isotype subgroups of global mixed groups. Our goal is to advance the theory of -isotype subgroups to a level comparable to its status in the simpler contexts of torsion-free and -local mixed groups. Given the history of those theories, one anticipates that definitive results are to be found only when attention is restricted to global -groups, the prototype being global groups with decomposition bases. A large portion of this paper is...