Formalized Mathematics
(ISSN 1426-2630)
Volume 14, Number 1 (2006):
PDF.
- Yatsuka Nakamura.
Determinant of Some Matrices of Field Elements,
Formalized Mathematics 14(1), pages 1-5, 2006. MML Identifier: MATRIX_7
Summary: Here, we present determinants of some square matrices of field elements. First, the determinat of $2*2$ matrix is shown. Secondly, the determinants of zero matrix and unit matrix are shown, which are equal to 0 in the field and 1 in the field respectively. Thirdly, the determinant of diagonal matrix is shown, which is a product of all diagonal elements of the matrix. At the end, we prove that the determinant of a matrix is same as the determinant of its transpose.
- Xiaopeng Yue, Dahai Hu, Xiquan Liang.
Some Properties of Some Special Matrices. Part II,
Formalized Mathematics 14(1), pages 7-12, 2006. MML Identifier: MATRIX_8
Summary: This article describes definitions of Idempotent Matrix, Nilpotent Matrix, Involutory Matrix, Self Reversible Matrix, Similar Matrix, Congruent Matrix, the Trace of a Matrix and their main properties.
- Ewa Romanowicz, Adam Grabowski.
On the Permanent of a Matrix,
Formalized Mathematics 14(1), pages 13-20, 2006. MML Identifier: MATRIX_9
Summary: We introduce the notion of a permanent 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.
- Yatsuka Nakamura, Nobuyuki Tamura, Wenpai Chang.
A Theory of Matrices of Real Elements,
Formalized Mathematics 14(1), pages 21-28, 2006. MML Identifier: MATRIXR1
Summary: 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. The linearity of such product is shown.
- Magdalena Jastrzcebska, Adam Grabowski.
On the Properties of the M\"obius Function,
Formalized Mathematics 14(1), pages 29-36, 2006. MML Identifier: MOEBIUS1
Summary: We formalized some basic properties of the M\"obius function which is defined classically as $$\mu(n) = \begin{cases} 1, \textrm{~if~} n = 1,\\ 0, \textrm{~if~}p^2|n \textrm{~for~some~prime~}p\\ (-1)^r, \textrm{~if~}n=p_1 p_2 \cdots p_r, \textrm{~where~} p_i \textrm{~are~distinct~primes.}\\ \end{cases},$$ as e.g., its multiplicativity. To enable smooth reasoning about the sum of this number-theoretic function, we introduced an underlying manysorted set indexed by natural numbers. Its elements are just values of the M\"obius function.\par 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.\par 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 \cite{HardyWright}.
- Bo Li, Yan Zhang, Xiquan Liang.
Several Differentiation Formulas of Special Functions. Part III,
Formalized Mathematics 14(1), pages 37-45, 2006. MML Identifier: FDIFF_7
Summary: In this article, we give several differentiation formulas of special and composite functions including trigonometric function, inverse trigonometric function, polynomial function and logarithmic function.