:: Ring IdealsPRE_CIRC,
:: by Jonathan Backer , Piotr Rudnicki and Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem Th1: :: IDEAL_1:1
:: deftheorem Def1 defines add-closed IDEAL_1:def 1 :
:: deftheorem Def2 defines left-ideal IDEAL_1:def 2 :
:: deftheorem Def3 defines right-ideal IDEAL_1:def 3 :
theorem Th2: :: IDEAL_1:2
theorem Th3: :: IDEAL_1:3
theorem Th4: :: IDEAL_1:4
theorem Th5: :: IDEAL_1:5
theorem Th6: :: IDEAL_1:6
theorem :: IDEAL_1:7
theorem :: IDEAL_1:8
theorem :: IDEAL_1:9
theorem Th10: :: IDEAL_1:10
theorem Th11: :: IDEAL_1:11
theorem Th12: :: IDEAL_1:12
:: deftheorem defines trivial IDEAL_1:def 4 :
theorem Th13: :: IDEAL_1:13
theorem Th14: :: IDEAL_1:14
theorem :: IDEAL_1:15
theorem :: IDEAL_1:16
theorem Th17: :: IDEAL_1:17
theorem :: IDEAL_1:18
:: deftheorem IDEAL_1:def 5 :
canceled;
:: deftheorem defines add| IDEAL_1:def 6 :
:: deftheorem defines mult| IDEAL_1:def 7 :
:: deftheorem defines Gr IDEAL_1:def 8 :
Lm1:
for R being comRing
for a being Element of R holds { (a * r) where r is Element of R : verum } is Ideal of R
theorem Th19: :: IDEAL_1:19
theorem :: IDEAL_1:20
theorem :: IDEAL_1:21
theorem :: IDEAL_1:22
:: deftheorem Def9 defines LinearCombination IDEAL_1:def 9 :
:: deftheorem Def10 defines LeftLinearCombination IDEAL_1:def 10 :
:: deftheorem Def11 defines RightLinearCombination IDEAL_1:def 11 :
theorem Th23: :: IDEAL_1:23
theorem Th24: :: IDEAL_1:24
theorem Th25: :: IDEAL_1:25
theorem Th26: :: IDEAL_1:26
theorem :: IDEAL_1:27
theorem Th28: :: IDEAL_1:28
theorem Th29: :: IDEAL_1:29
theorem :: IDEAL_1:30
theorem Th31: :: IDEAL_1:31
theorem Th32: :: IDEAL_1:32
theorem Th33: :: IDEAL_1:33
theorem Th34: :: IDEAL_1:34
:: deftheorem Def12 defines represents IDEAL_1:def 12 :
theorem :: IDEAL_1:35
theorem :: IDEAL_1:36
:: deftheorem Def13 defines represents IDEAL_1:def 13 :
theorem :: IDEAL_1:37
theorem :: IDEAL_1:38
:: deftheorem Def14 defines represents IDEAL_1:def 14 :
theorem :: IDEAL_1:39
theorem :: IDEAL_1:40
theorem :: IDEAL_1:41
theorem :: IDEAL_1:42
theorem :: IDEAL_1:43
:: deftheorem Def15 defines -Ideal IDEAL_1:def 15 :
:: deftheorem Def16 defines -LeftIdeal IDEAL_1:def 16 :
:: deftheorem Def17 defines -RightIdeal IDEAL_1:def 17 :
theorem Th44: :: IDEAL_1:44
theorem Th45: :: IDEAL_1:45
theorem Th46: :: IDEAL_1:46
:: deftheorem defines Basis IDEAL_1:def 18 :
theorem :: IDEAL_1:47
theorem :: IDEAL_1:48
theorem :: IDEAL_1:49
theorem :: IDEAL_1:50
theorem :: IDEAL_1:51
theorem :: IDEAL_1:52
theorem :: IDEAL_1:53
theorem :: IDEAL_1:54
theorem :: IDEAL_1:55
theorem :: IDEAL_1:56
theorem Th57: :: IDEAL_1:57
theorem :: IDEAL_1:58
theorem :: IDEAL_1:59
theorem Th60: :: IDEAL_1:60
theorem Th61: :: IDEAL_1:61
theorem Th62: :: IDEAL_1:62
theorem Th63: :: IDEAL_1:63
theorem Th64: :: IDEAL_1:64
theorem Th65: :: IDEAL_1:65
theorem Th66: :: IDEAL_1:66
theorem :: IDEAL_1:67
Lm2:
for a, b being set holds {a} c= {a,b}
theorem :: IDEAL_1:68
theorem :: IDEAL_1:69
:: deftheorem defines * IDEAL_1:def 19 :
theorem Th70: :: IDEAL_1:70
theorem :: IDEAL_1:71
:: deftheorem defines + IDEAL_1:def 20 :
theorem :: IDEAL_1:72
theorem Th73: :: IDEAL_1:73
theorem Th74: :: IDEAL_1:74
theorem :: IDEAL_1:75
theorem :: IDEAL_1:76
:: deftheorem defines /\ IDEAL_1:def 21 :
theorem :: IDEAL_1:77
canceled;
theorem :: IDEAL_1:78
canceled;
theorem :: IDEAL_1:79
canceled;
theorem :: IDEAL_1:80
:: deftheorem defines *' IDEAL_1:def 22 :
theorem :: IDEAL_1:81
theorem Th82: :: IDEAL_1:82
theorem Th83: :: IDEAL_1:83
theorem Th84: :: IDEAL_1:84
theorem :: IDEAL_1:85
:: deftheorem Def23 defines are_co-prime IDEAL_1:def 23 :
theorem Th86: :: IDEAL_1:86
theorem :: IDEAL_1:87
:: deftheorem defines % IDEAL_1:def 24 :
theorem :: IDEAL_1:88
theorem :: IDEAL_1:89
theorem Th90: :: IDEAL_1:90
theorem :: IDEAL_1:91
theorem :: IDEAL_1:92
theorem :: IDEAL_1:93
:: deftheorem defines sqrt IDEAL_1:def 25 :
theorem :: IDEAL_1:94
theorem :: IDEAL_1:95
:: deftheorem Def26 defines finitely_generated IDEAL_1:def 26 :
:: deftheorem Def27 defines Noetherian IDEAL_1:def 27 :
:: deftheorem Def28 defines principal IDEAL_1:def 28 :
:: deftheorem Def29 defines PID IDEAL_1:def 29 :
theorem Th96: :: IDEAL_1:96
theorem Th97: :: IDEAL_1:97
theorem Th98: :: IDEAL_1:98
theorem :: IDEAL_1:99
theorem :: IDEAL_1:100
theorem :: IDEAL_1:101
theorem :: IDEAL_1:102