:: A Theory of Matrices of Complex Elements
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received December 10, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: MATRIX_5:1
theorem :: MATRIX_5:2
:: deftheorem defines COMPLEX2Field MATRIX_5:def 1 :
:: deftheorem defines Field2COMPLEX MATRIX_5:def 2 :
theorem :: MATRIX_5:3
theorem :: MATRIX_5:4
theorem :: MATRIX_5:5
theorem :: MATRIX_5:6
:: deftheorem defines + MATRIX_5:def 3 :
:: deftheorem defines - MATRIX_5:def 4 :
:: deftheorem defines - MATRIX_5:def 5 :
:: deftheorem defines * MATRIX_5:def 6 :
:: deftheorem Def7 defines * MATRIX_5:def 7 :
theorem :: MATRIX_5:7
theorem :: MATRIX_5:8
theorem :: MATRIX_5:9
canceled;
theorem Th10: :: MATRIX_5:10
theorem :: MATRIX_5:11
theorem :: MATRIX_5:12
theorem Th13: :: MATRIX_5:13
theorem :: MATRIX_5:14
theorem :: MATRIX_5:15
:: deftheorem defines 0_Cx MATRIX_5:def 8 :
theorem :: MATRIX_5:16
theorem :: MATRIX_5:17
canceled;
theorem :: MATRIX_5:18
canceled;
theorem :: MATRIX_5:19
canceled;
theorem :: MATRIX_5:20
canceled;
theorem :: MATRIX_5:21
theorem :: MATRIX_5:22
canceled;
theorem :: MATRIX_5:23
theorem :: MATRIX_5:24
canceled;
theorem :: MATRIX_5:25
theorem :: MATRIX_5:26
canceled;
theorem :: MATRIX_5:27
canceled;
theorem :: MATRIX_5:28
canceled;
theorem :: MATRIX_5:29
canceled;
theorem :: MATRIX_5:30
canceled;
theorem :: MATRIX_5:31
canceled;
theorem :: MATRIX_5:32
canceled;
theorem :: MATRIX_5:33
canceled;
theorem :: MATRIX_5:34
canceled;
theorem :: MATRIX_5:35
theorem Th36: :: MATRIX_5:36
theorem :: MATRIX_5:37
theorem Th38: :: MATRIX_5:38
theorem :: MATRIX_5:39
theorem Th40: :: MATRIX_5:40
theorem :: MATRIX_5:41
theorem :: MATRIX_5:42