src/HOL/Algebra/Ideal.thy
changeset 67443 3abf6a722518
parent 63633 2accfb71e33b
child 68443 43055b016688
     1.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Jan 16 09:12:16 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Jan 16 09:30:00 2018 +0100
     1.3 @@ -828,7 +828,7 @@
     1.4  
     1.5  subsection \<open>Derived Theorems\<close>
     1.6  
     1.7 -\<comment>"A non-zero cring that has only the two trivial ideals is a field"
     1.8 +\<comment> \<open>A non-zero cring that has only the two trivial ideals is a field\<close>
     1.9  lemma (in cring) trivialideals_fieldI:
    1.10    assumes carrnzero: "carrier R \<noteq> {\<zero>}"
    1.11      and haveideals: "{I. ideal I R} = {{\<zero>}, carrier R}"
    1.12 @@ -921,7 +921,7 @@
    1.13    qed
    1.14  qed (simp add: zeroideal oneideal)
    1.15  
    1.16 -\<comment>"Jacobson Theorem 2.2"
    1.17 +\<comment> \<open>Jacobson Theorem 2.2\<close>
    1.18  lemma (in cring) trivialideals_eq_field:
    1.19    assumes carrnzero: "carrier R \<noteq> {\<zero>}"
    1.20    shows "({I. ideal I R} = {{\<zero>}, carrier R}) = field R"