begin
theorem Th1:
begin
:: 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:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines trivial IDEAL_1:def 4 :
theorem Th13:
theorem Th14:
theorem
theorem
theorem Th17:
theorem
:: 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:
theorem
theorem
theorem
begin
:: 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:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: deftheorem Def12 defines represents IDEAL_1:def 12 :
theorem
theorem
:: deftheorem Def13 defines represents IDEAL_1:def 13 :
theorem
theorem
:: deftheorem Def14 defines represents IDEAL_1:def 14 :
theorem
theorem
theorem
theorem
theorem
begin
:: 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:
theorem Th45:
theorem Th46:
:: deftheorem defines Basis IDEAL_1:def 18 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th57:
theorem
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
Lm2:
for a, b being set holds {a} c= {a,b}
theorem
theorem
begin
:: deftheorem defines * IDEAL_1:def 19 :
theorem Th70:
theorem
:: deftheorem defines + IDEAL_1:def 20 :
theorem
theorem Th73:
theorem Th74:
theorem
theorem
:: deftheorem defines /\ IDEAL_1:def 21 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines *' IDEAL_1:def 22 :
theorem
theorem Th82:
theorem Th83:
theorem Th84:
theorem
:: deftheorem Def23 defines are_co-prime IDEAL_1:def 23 :
theorem Th86:
theorem
:: deftheorem defines % IDEAL_1:def 24 :
theorem
theorem
theorem Th90:
theorem
theorem
theorem
:: deftheorem defines sqrt IDEAL_1:def 25 :
theorem
theorem
begin
:: 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:
theorem Th97:
theorem Th98:
theorem
theorem
theorem
theorem