http://hdl.handle.net/11320/8761 Thu, 29 Oct 2026 13:53:30 GMT 2026-10-29T13:53:30Z 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/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 http://hdl.handle.net/11320/21342 Tytuł: Basic Properties of Determinants of Square Matrices over a Field Autorzy: Pąk, Karol Abstrakt: In this paper I present basic properties of the determinant of square matrices over a field and selected properties of the sign of a permutation. First, I define the sign of a permutation by the requirement where p is any fixed permutation of a set with n elements. I prove that the sign of a product of two permutations is the same as the product of their signs and show the relation between signs and parity of permutations. Then I consider the determinant of a linear combination of lines, the determinant of a matrix with permutated lines and the determinant of a matrix with a repeated line. Finally, at the end I prove that the determinant of a product of two square matrices is equal to the product of their determinants. Mon, 01 Jan 2007 00:00:00 GMT http://hdl.handle.net/11320/21342 2007-01-01T00:00:00Z http://hdl.handle.net/11320/21069 Tytuł: Orthomodular Lattices Autorzy: Mądra, Elżbieta; Grabowski, Adam Abstrakt: The main result of the article is the solution to the problem of short axiomatizations of orthomodular ortholattices. Based on EQP/Otter results [10], we gave a set of three equations which is equivalent to the classical, much longer equational basis of such a class. Also the basic example of the lattice which is not orthomodular, i.e. benzene (or B6) is defined in two settings– as a relational structure (poset) and as a lattice. As a preliminary work, we present the proofs of the dependence of other axiomatizations of ortholattices. The formalization of the properties of orthomodular lattices follows [4]. Tue, 01 Jan 2008 00:00:00 GMT http://hdl.handle.net/11320/21069 2008-01-01T00:00:00Z