http://hdl.handle.net/11320/21345 Thu, 29 Oct 2026 21:54:31 GMT 2026-10-29T21:54:31Z http://hdl.handle.net/11320/21360 Tytuł: Several Differentiation Formulas of Special Functions. Part II Autorzy: Li, Bo; Zhang, Yan; Liang, Xiquan Abstrakt: In this article, we give several differentiation formulas of special and composite functions including trigonometric function, inverse trigonometric function, polynomial function and logarithmic function. Sun, 01 Jan 2006 00:00:00 GMT http://hdl.handle.net/11320/21360 2006-01-01T00:00:00Z http://hdl.handle.net/11320/21358 Tytuł: On the Properties of the Möbius Function Autorzy: Jastrzębska, Magdalena; Grabowski, Adam Abstrakt: We formalized some basic properties of the Möbius function which is defined classically as μ(n) = 1, if n = 1; μ(n) = 0, if p² | n for some prime p; μ(n) = (−1)ʳ, if n = p₁p₂⋯pᵣ, where pᵢ are distinct primes, as e.g., its multiplicativity. To enable smooth reasoning about the sum of this number-theoretic function, we introduced an underlying many-sorted set indexed by the set of natural numbers. Its elements are just values of the Möbius function. The second part of the paper is devoted to the notion of the radical of number, i.e. the product of its all prime factors. The formalization (which is very much like the one developed in Isabelle proof assistant connected with Avigad’s formal proof of Prime Number Theorem) was done according to the book [13]. Opis: This is a part of the author's MSc thesis. Sun, 01 Jan 2006 00:00:00 GMT http://hdl.handle.net/11320/21358 2006-01-01T00:00:00Z http://hdl.handle.net/11320/21357 Tytuł: A Theory of Matrices of Real Elements Autorzy: Nakamura, Yatsuka; Tamura, Nobuyuki; Chang, Wenpai Abstrakt: Here, the concept of matrix of real elements is introduced. This is defined as a special case of the general concept of matrix of a field. For such a real matrix, the notions of addition, subtraction, scalar product are defined. For any real finite sequences, two transformations to matrices are introduced. One of the matrices is of width 1, and the other is of length 1. By such transformations, two products of a matrix and a finite sequence are defined. Also the linearity of such product is shown. Sun, 01 Jan 2006 00:00:00 GMT http://hdl.handle.net/11320/21357 2006-01-01T00:00:00Z http://hdl.handle.net/11320/21354 Tytuł: On the Permanent of a Matrix Autorzy: Romanowicz, Ewa; Grabowski, Adam Abstrakt: We introduce the notion of a permanent [13] of a square matrix. It is a notion somewhat related to a determinant, so we follow closely the approach and theorems already introduced in the Mizar Mathematical Library for the determinant. Unfortunately, the formalization of the latter notion is at its early stage, so we had to prove many very elementary auxiliary facts. Opis: This is a part of the author's MSc thesis. Sun, 01 Jan 2006 00:00:00 GMT http://hdl.handle.net/11320/21354 2006-01-01T00:00:00Z