Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

Product of Families of Groups and Vector Spaces


Anna Lango
Warsaw University, Bialystok
Grzegorz Bancerek
Polish Academy of Sciences, Institute of Mathematics, Warsaw

Summary.

In the first section we present properties of fields and Abelian groups in terms of commutativity, associativity, etc. Next, we are concerned with operations on $n$-tuples on some set which are generalization of operations on this set. It is used in third section to introduce the $n$-power of a group and the $n$-power of a field. Besides, we introduce a concept of indexed family of binary (unary) operations over some indexed family of sets and a product of such families which is binary (unary) operation on a product of family sets. We use that product in the last section to introduce the product of a finite sequence of Abelian groups.

MML Identifier: PRVECT_1

The terminology and notation used in this paper have been introduced in the following articles [13] [7] [16] [1] [17] [5] [6] [4] [11] [15] [10] [8] [3] [14] [2] [12] [9]

Contents (PDF format)

  1. Abelian Groups and Fields
  2. The $n$-Product of a Binary and a Unary Operation
  3. The $n$-Power of a Group and of a Field
  4. Sequences of Non-empty Sets
  5. The Product of Families of Operations
  6. The Product of Families of Groups

Bibliography

[1] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.
[2] Grzegorz Bancerek. Cartesian product of functions. Journal of Formalized Mathematics, 3, 1991.
[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. Binary operations applied to finite sequences. Journal of Formalized Mathematics, 2, 1990.
[9] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
[10] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
[11] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.
[12] Andrzej Trybulec. Semilattice operations on finite subsets. Journal of Formalized Mathematics, 1, 1989.
[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[14] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.
[15] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[16] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[17] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received December 29, 1992


[ Download a postscript version, MML identifier index, Mizar home page]