Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Construction of Finite Sequence over Ring and Left-, Right-, and Bi-Modules over a Ring


Michal Muzalewski
Warsaw University, Bialystok
Leslaw W. Szczerba
Siedlce University

Summary.

This text includes definitions of finite sequences over rings and left-, right-, and bi-module over a ring treated as functions defined for {\sl all} natural numbers, but with almost everywhere equal to zero. Some elementary theorems are proved, in particular for each category of sequences the scheme about existence is proved. In all four cases, i.e. for rings, left-, right and bi- modules are almost exactly the same, hovewer we do not know how to do the job in Mizar in a different way. The paper is mostly based on the paper [2]. In particular the notion of initial segment of natural numbers is introduced which differs from that of [2] by starting with zero. This proved to be more convenient for algebraic purposes.

Supported by RPBP.III-24.C3.

MML Identifier: ALGSEQ_1

The terminology and notation used in this paper have been introduced in the following articles [6] [9] [7] [1] [10] [3] [8] [4] [5]

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[5] Jan Popiolek. Real normed space. Journal of Formalized Mathematics, 2, 1990.
[6] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[7] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[8] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.
[9] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[10] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received September 13, 1990


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