http://hdl.handle.net/11320/14664 2026-06-01T19:16:23Z http://hdl.handle.net/11320/14679 Tytuł: Elementary Number Theory Problems. Part VI Autorzy: Grabowski, Adam Abstrakt: This paper reports on the formalization in Mizar system [1], [2]of ten selected problems from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [7] (see [6] for details of this concrete dataset). This article is devoted mainly to arithmetic progressions: problems 52, 54, 55, 56, 60, 64, 70,71, and 73 belong to the chapter “Arithmetic Progressions”, and problem 50 is from “Relatively Prime Numbers”. 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14677 Tytuł: Elementary Number Theory Problems. Part V Autorzy: Korniłowicz, Artur; Naumowicz, Adam Abstrakt: This paper reports on the formalization of ten selected problems from W. Sierpinski’s book “250 Problems in Elementary Number Theory”[5] using the Mizar system [4], [1], [2]. Problems 12, 13, 31, 32, 33, 35 and 40 belong to the chapter devoted to the divisibility of numbers, problem 47 concerns relatively prime numbers, whereas problems 76 and 79 are taken from the chapter on prime and composite numbers. 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14676 Tytuł: Elementary Number Theory Problems. Part IV Autorzy: Korniłowicz, Artur Abstrakt: In this paper problems 17, 18, 26, 27, 28, and 98 from [9] are formalized, using the Mizar formalism [8], [2], [3], [6]. 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14675 Tytuł: Ring of Endomorphisms and Modules over a Ring Autorzy: Watase, Yasushige Abstrakt: We formalize in the Mizar system [3], [4] some basic propertieson left module over a ring such as constructing a module via a ring of endomor-phism of an abelian group and the set of all homomorphisms of modules form amodule [1] along with Ch. 2 set. 1 of [2]. The formalized items are shown in the below list with notations: M ab for an Abelian group with a suffix “ab” and M without a suffix is used for left modules over a ring. 1. The endomorphism ring of an abelian group denoted by End (M ab). 2. A pair of an Abelian group M ab and a ring homomorphism Rρ→End (M ab) determines a left R-module, formalized as a function AbGrLMod(M ab,ρ) in the article. 3. The set of all functions from MtoNformR-module and denoted by FuncModR(M,N). 4. The set R-module homomorphisms of M to N, denoted by HomR (M,N),forms R-module. 5. A formal proof of HomR( ̄R,M)∼=Mis given, where the ̄Rdenotes theregular representation of R, i.e. we regard R it self as a left R-module. 6. A formal proof of AbGrLMod(M′ab,ρ′)∼=M where M′ab is an abelian group obtained by removing the scalar multiplication from M, and ρ′ is obtained by currying the scalar multiplication of M. The removal of the multiplication from M has been done by the forgettable functor defined as AbGrin the article. 2022-01-01T00:00:00Z