:: Calculation of Matrices of Field Elements. Part {I}
:: by Yatsuka Nakamura and Hiroshi Yamazaki
::
:: Received August 8, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem defines - MATRIX_4:def 1 :
for
K being
Field for
M1,
M2 being
Matrix of
K holds
M1 - M2 = M1 + (- M2);
theorem Th1: :: MATRIX_4:1
theorem Th2: :: MATRIX_4:2
theorem :: MATRIX_4:3
theorem :: MATRIX_4:4
theorem :: MATRIX_4:5
theorem :: MATRIX_4:6
theorem Th7: :: MATRIX_4:7
theorem Th8: :: MATRIX_4:8
theorem Th9: :: MATRIX_4:9
theorem :: MATRIX_4:10
theorem Th11: :: MATRIX_4:11
theorem Th12: :: MATRIX_4:12
theorem :: MATRIX_4:13
theorem Th14: :: MATRIX_4:14
theorem Th15: :: MATRIX_4:15
theorem Th16: :: MATRIX_4:16
theorem :: MATRIX_4:17
theorem Th18: :: MATRIX_4:18
theorem :: MATRIX_4:19
theorem Th20: :: MATRIX_4:20
theorem Th21: :: MATRIX_4:21
theorem Th22: :: MATRIX_4:22
theorem :: MATRIX_4:23
theorem :: MATRIX_4:24
theorem :: MATRIX_4:25
theorem Th26: :: MATRIX_4:26
theorem :: MATRIX_4:27
theorem Th28: :: MATRIX_4:28
theorem :: MATRIX_4:29
theorem :: MATRIX_4:30
theorem Th31: :: MATRIX_4:31
theorem :: MATRIX_4:32
theorem :: MATRIX_4:33
theorem :: MATRIX_4:34
theorem :: MATRIX_4:35
theorem :: MATRIX_4:36
theorem :: MATRIX_4:37
theorem Th38: :: MATRIX_4:38
theorem :: MATRIX_4:39
theorem :: MATRIX_4:40
theorem :: MATRIX_4:41
theorem :: MATRIX_4:42
theorem :: MATRIX_4:43
theorem Th44: :: MATRIX_4:44
theorem :: MATRIX_4:45
theorem Th46: :: MATRIX_4:46
theorem Th47: :: MATRIX_4:47
theorem :: MATRIX_4:48
theorem :: MATRIX_4:49
theorem :: MATRIX_4:50
theorem :: MATRIX_4:51
theorem :: MATRIX_4:52
theorem :: MATRIX_4:53
theorem :: MATRIX_4:54
theorem Th55: :: MATRIX_4:55
theorem Th56: :: MATRIX_4:56
theorem Th57: :: MATRIX_4:57
theorem :: MATRIX_4:58
theorem Th59: :: MATRIX_4:59
theorem Th60: :: MATRIX_4:60
theorem Th61: :: MATRIX_4:61
theorem :: MATRIX_4:62
theorem :: MATRIX_4:63
theorem :: MATRIX_4:64