The Properties Of Generalized Circulant Matrix And The Realization Of Circulant Matrix In Mizar System

The circulant matrix belongs to the Teoplitz matrix class. For n×nTeoplitz matrix, it has 2n-1 elements, the elements on the line parallelingthe main diagonal line are the same. The circulant matrix has more specialproperties: for n×n circulant matrix, it only has n elements; itsarbitrary line comes from the permutation of the first line, and so on.Because of its special structure and good properties, the research of itwill bring out a lot of meaningful results.The Mizar system is one of the fifteen famous automated mathematicaltheorem proving systems. It has developed for thirty years by the leadingof Pro. Andrzej trublyc of Plock science association. It has formed selfcontained formalization system of mathematical knowledge which almostcovers all the branches of mathematical. Compared with the huge repositoryof mathematics, there are many areas needed to explore and study.In this paper, we discuss the diagonalization of generalized circulantmatrix by using generalized vandermonde matrix. Then get some relatedproperties of generalized circulant matrix. After that discuss somealgorithms of reversing of generalized circulation matrices. At last wegive the definition of circulant matrix in Mizar system by using finitesequence and give the determination of some basic properties of circulantmatrix in Mizar system.This article contains three chapters: Chapter 1: give relative knowledge about this article. Mainlyintroduce the development of the studying of circulantmatrix, the basic conception and properties of circulantmatrix and the introduction of Mizar system.Chapter 2: discuss the diagonalization of generalized circulantmatrix by using generalized Vandermonde matrix, and thendiscuss some algorithms of reversing of generalizedcirculation matrixes.Chapter 3: give the definition of circulant matrix in Mizar systemby using finite sequence and enrich the content of MizarMathematical Library.