:: Some Properties Of Some Special Matrices
:: by Xiaopeng Yue , Xiquan Liang and Zhongpin Sun
::
:: Received December 7, 2005
:: Copyright (c) 2005 Association of Mizar Users
:: deftheorem Def1 defines commutes_with MATRIX_6:def 1 :
:: deftheorem Def2 defines is_reverse_of MATRIX_6:def 2 :
:: deftheorem Def3 defines invertible MATRIX_6:def 3 :
theorem Th1: :: MATRIX_6:1
theorem Th2: :: MATRIX_6:2
theorem Th3: :: MATRIX_6:3
theorem :: MATRIX_6:4
theorem :: MATRIX_6:5
theorem Th6: :: MATRIX_6:6
theorem Th7: :: MATRIX_6:7
:: deftheorem Def4 defines ~ MATRIX_6:def 4 :
theorem Th8: :: MATRIX_6:8
theorem :: MATRIX_6:9
theorem Th10: :: MATRIX_6:10
theorem :: MATRIX_6:11
theorem :: MATRIX_6:12
theorem :: MATRIX_6:13
theorem :: MATRIX_6:14
theorem :: MATRIX_6:15
theorem Th16: :: MATRIX_6:16
theorem :: MATRIX_6:17
theorem :: MATRIX_6:18
theorem :: MATRIX_6:19
:: deftheorem Def5 defines symmetric MATRIX_6:def 5 :
theorem :: MATRIX_6:20
canceled;
theorem Th21: :: MATRIX_6:21
theorem :: MATRIX_6:22
theorem :: MATRIX_6:23
theorem Th24: :: MATRIX_6:24
for
n being
Nat for
K being
Field for
M1,
M2 being
Matrix of
n,
K holds
(M1 + M2) @ = (M1 @ ) + (M2 @ )
theorem :: MATRIX_6:25
theorem :: MATRIX_6:26
theorem Th27: :: MATRIX_6:27
theorem :: MATRIX_6:28
theorem :: MATRIX_6:29
:: deftheorem Def6 defines antisymmetric MATRIX_6:def 6 :
theorem :: MATRIX_6:30
theorem :: MATRIX_6:31
theorem :: MATRIX_6:32
theorem :: MATRIX_6:33
theorem :: MATRIX_6:34
theorem :: MATRIX_6:35
theorem :: MATRIX_6:36
theorem Th37: :: MATRIX_6:37
theorem :: MATRIX_6:38
theorem :: MATRIX_6:39
theorem :: MATRIX_6:40
theorem Th41: :: MATRIX_6:41
:: deftheorem Def7 defines Orthogonal MATRIX_6:def 7 :
theorem Th42: :: MATRIX_6:42
theorem Th43: :: MATRIX_6:43
theorem :: MATRIX_6:44
theorem :: MATRIX_6:45
theorem Th46: :: MATRIX_6:46
theorem :: MATRIX_6:47
theorem :: MATRIX_6:48
theorem :: MATRIX_6:49
theorem :: MATRIX_6:50
theorem :: MATRIX_6:51
theorem :: MATRIX_6:52
theorem :: MATRIX_6:53
canceled;
theorem :: MATRIX_6:54
theorem :: MATRIX_6:55
theorem :: MATRIX_6:56
theorem :: MATRIX_6:57
theorem Th58: :: MATRIX_6:58
theorem :: MATRIX_6:59
theorem :: MATRIX_6:60
theorem :: MATRIX_6:61