Displaying similar documents to “Permutation matrices and matrix equivalence over a finite field.”

Basic Properties of Determinants of Square Matrices over a Field 1

Karol Pąk (2007)

Formalized Mathematics

Similarity:

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...

On the Permanent of a Matrix

Ewa Romanowicz, Adam Grabowski (2006)

Formalized Mathematics

Similarity:

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.