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"
```