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

## Sum and Product of Finite Sequences of Elements of a Field

Katarzyna Zawadzka
Warsaw University, Bialystok

### Summary.

This article is concerned with a generalization of concepts introduced in , i.e., there are introduced the sum and the product of finite number of elements of any field. Moreover, the product of vectors which yields a vector is introduced. According to , some operations on \$i\$-tuples of elements of field are introduced: addition, subtraction, and complement. Some properties of the sum and the product of finite number of elements of a field are present.

#### MML Identifier: FVSUM_1

The terminology and notation used in this paper have been introduced in the following articles                      

#### Contents (PDF format)

1. Auxiliary theorems
2. Some operations on \$i\$-tuples
3. The sum of finite number of elements
4. The product of finite number of elements
5. The product of vectors

#### Acknowledgments

I would like to thank Czes{\l}aw Byli\'nski for his help.

#### Bibliography

 Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
 Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
 Czeslaw Bylinski. Binary operations applied to finite sequences. Journal of Formalized Mathematics, 2, 1990.
 Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.
 Czeslaw Bylinski. Semigroup operations on finite subsets. Journal of Formalized Mathematics, 2, 1990.
 Czeslaw Bylinski. The sum and product of finite sequences of real numbers. Journal of Formalized Mathematics, 2, 1990.
 Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
 Katarzyna Jankowska. Transpose matrices and groups of permutations. Journal of Formalized Mathematics, 4, 1992.
 Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.
 Michal Muzalewski and Wojciech Skaba. From loops to abelian multiplicative groups with zero. Journal of Formalized Mathematics, 2, 1990.
 Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.
 Andrzej Trybulec. Semilattice operations on finite subsets. Journal of Formalized Mathematics, 1, 1989.
 Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
 Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
 Andrzej Trybulec and Agata Darmochwal. Boolean domains. Journal of Formalized Mathematics, 1, 1989.
 Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
 Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
 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]