:: Commutator and Center of a Group
:: by Wojciech A. Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: GROUP_5:1
theorem :: GROUP_5:2
theorem Th3: :: GROUP_5:3
theorem Th4: :: GROUP_5:4
theorem Th5: :: GROUP_5:5
theorem :: GROUP_5:6
theorem Th7: :: GROUP_5:7
theorem :: GROUP_5:8
:: deftheorem Def1 defines |^ GROUP_5:def 1 :
theorem :: GROUP_5:9
canceled;
theorem :: GROUP_5:10
canceled;
theorem :: GROUP_5:11
canceled;
theorem Th12: :: GROUP_5:12
theorem Th13: :: GROUP_5:13
theorem Th14: :: GROUP_5:14
theorem Th15: :: GROUP_5:15
theorem :: GROUP_5:16
theorem Th17: :: GROUP_5:17
theorem Th18: :: GROUP_5:18
:: deftheorem defines [. GROUP_5:def 2 :
theorem Th19: :: GROUP_5:19
theorem Th20: :: GROUP_5:20
theorem :: GROUP_5:21
theorem Th22: :: GROUP_5:22
theorem Th23: :: GROUP_5:23
theorem :: GROUP_5:24
theorem Th25: :: GROUP_5:25
theorem Th26: :: GROUP_5:26
theorem :: GROUP_5:27
theorem Th28: :: GROUP_5:28
theorem :: GROUP_5:29
theorem Th30: :: GROUP_5:30
theorem Th31: :: GROUP_5:31
theorem :: GROUP_5:32
theorem :: GROUP_5:33
theorem :: GROUP_5:34
theorem :: GROUP_5:35
theorem :: GROUP_5:36
theorem :: GROUP_5:37
theorem :: GROUP_5:38
theorem Th39: :: GROUP_5:39
Lm1:
for G being commutative Group
for a, b being Element of G holds a * b = b * a
;
theorem :: GROUP_5:40
theorem Th41: :: GROUP_5:41
:: deftheorem defines [. GROUP_5:def 3 :
theorem :: GROUP_5:42
canceled;
theorem :: GROUP_5:43
theorem :: GROUP_5:44
theorem :: GROUP_5:45
theorem :: GROUP_5:46
theorem :: GROUP_5:47
theorem :: GROUP_5:48
theorem :: GROUP_5:49
theorem :: GROUP_5:50
:: deftheorem defines commutators GROUP_5:def 4 :
theorem :: GROUP_5:51
canceled;
theorem Th52: :: GROUP_5:52
theorem :: GROUP_5:53
theorem :: GROUP_5:54
theorem Th55: :: GROUP_5:55
theorem Th56: :: GROUP_5:56
:: deftheorem defines commutators GROUP_5:def 5 :
theorem :: GROUP_5:57
canceled;
theorem Th58: :: GROUP_5:58
theorem Th59: :: GROUP_5:59
theorem :: GROUP_5:60
theorem Th61: :: GROUP_5:61
theorem Th62: :: GROUP_5:62
theorem Th63: :: GROUP_5:63
:: deftheorem defines commutators GROUP_5:def 6 :
theorem :: GROUP_5:64
canceled;
theorem Th65: :: GROUP_5:65
theorem :: GROUP_5:66
:: deftheorem defines [. GROUP_5:def 7 :
theorem :: GROUP_5:67
canceled;
theorem Th68: :: GROUP_5:68
theorem Th69: :: GROUP_5:69
theorem :: GROUP_5:70
:: deftheorem defines [. GROUP_5:def 8 :
theorem :: GROUP_5:71
canceled;
theorem :: GROUP_5:72
theorem :: GROUP_5:73
theorem Th74: :: GROUP_5:74
theorem :: GROUP_5:75
theorem :: GROUP_5:76
theorem Th77: :: GROUP_5:77
Lm2:
for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]
theorem Th78: :: GROUP_5:78
theorem Th79: :: GROUP_5:79
theorem :: GROUP_5:80
:: deftheorem defines ` GROUP_5:def 9 :
theorem :: GROUP_5:81
canceled;
theorem :: GROUP_5:82
theorem Th83: :: GROUP_5:83
theorem Th84: :: GROUP_5:84
theorem :: GROUP_5:85
theorem :: GROUP_5:86
:: deftheorem Def10 defines center GROUP_5:def 10 :
theorem :: GROUP_5:87
canceled;
theorem :: GROUP_5:88
canceled;
theorem Th89: :: GROUP_5:89
theorem :: GROUP_5:90
theorem :: GROUP_5:91
theorem :: GROUP_5:92
theorem :: GROUP_5:93
theorem :: GROUP_5:94