src/ZF/ex/Ring.thy

 (* Title:  ZF/ex/Ring.thy
 
 *)
 
-section {* Rings *}
+section \<open>Rings\<close>
 
 theory Ring imports Group begin
 
 no_notation
   cadd  (infixl "\<oplus>" 65) and

 
 lemma zero_eq [simp]: "zero(<C,M,I,A,Z,z>) = Z"
   by (simp add: zero_def)
 
 
-text {* Derived operations. *}
+text \<open>Derived operations.\<close>
 
 definition
   a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80) where
   "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
 

 
 locale abelian_monoid = fixes G (structure)
   assumes a_comm_monoid:
     "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
 
-text {*
+text \<open>
   The following definition is redundant but simple to use.
-*}
+\<close>
 
 locale abelian_group = abelian_monoid +
   assumes a_comm_group:
     "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
 

   assumes one_not_zero [simp]: "\<one> \<noteq> \<zero>"
     and integral: "\<lbrakk>a \<cdot> b = \<zero>; a \<in> carrier(R); b \<in> carrier(R)\<rbrakk> \<Longrightarrow>
                   a = \<zero> | b = \<zero>"
 
 
-subsection {* Basic Properties *}
+subsection \<open>Basic Properties\<close>
 
 lemma (in abelian_monoid) a_monoid:
      "monoid (<carrier(G), add_field(G), zero(G), 0>)"
 apply (insert a_comm_monoid)
 apply (simp add: comm_monoid_def)

   using comm_group.inv_mult [OF a_comm_group]
   by (simp add: a_inv_def ring_add_def [symmetric])
 
 lemmas (in abelian_monoid) a_ac = a_assoc a_comm a_lcomm
 
-text {*
+text \<open>
   The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
-*}
+\<close>
 
 context ring
 begin
 
 lemma l_null [simp]: "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"

   by (simp only: minus_def)
 
 end
 
 
-subsection {* Morphisms *}
+subsection \<open>Morphisms\<close>
 
 definition
   ring_hom :: "[i,i] => i" where
   "ring_hom(R,S) ==
     {h \<in> carrier(R) -> carrier(S).