Abstract
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.
Language: English
Page range: 13 - 20
Published on: Jun 13, 2008
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Related subjects:
© 2008 Ewa Romanowicz, Adam Grabowski, published by University of Białystok
This work is licensed under the Creative Commons License.