数字技术与应用
數字技術與應用
수자기술여응용
DIGITAL TECHNOLOGY AND APPLICATION
2011年
3期
114-116
,共3页
矩阵%Mizar%初等变换
矩陣%Mizar%初等變換
구진%Mizar%초등변환
本文在计算机上利用有限序列的复合映射给出了矩阵在Mizar系统下的定义,实现了可逆矩阵、对称和反对称矩阵、相似矩阵、合同矩阵等特殊矩阵的定义,给出了与上述矩阵有关的一些定理的计算机证明,并实现了矩阵的初等变换及相关运算.
本文在計算機上利用有限序列的複閤映射給齣瞭矩陣在Mizar繫統下的定義,實現瞭可逆矩陣、對稱和反對稱矩陣、相似矩陣、閤同矩陣等特殊矩陣的定義,給齣瞭與上述矩陣有關的一些定理的計算機證明,併實現瞭矩陣的初等變換及相關運算.
본문재계산궤상이용유한서렬적복합영사급출료구진재Mizar계통하적정의,실현료가역구진、대칭화반대칭구진、상사구진、합동구진등특수구진적정의,급출료여상술구진유관적일사정리적계산궤증명,병실현료구진적초등변환급상관운산.
