Loading theory "Localization_Ring.Localization"
locale Localization.submonoid
  fixes M :: "('a, 'b) monoid_scheme"  (structure)
    and S :: "'a set"
  assumes "Localization.submonoid M S"
locale mult_submonoid_of_rng
  fixes R :: "('a, 'b) ring_scheme"
    and S :: "'a set"
  assumes "mult_submonoid_of_rng R S"
locale mult_submonoid_of_crng
  fixes R :: "('a, 'b) ring_scheme"
    and S :: "'a set"
  assumes "mult_submonoid_of_crng R S"
locale eq_obj_rng_of_frac
  fixes R :: "('a, 'b) ring_scheme"  (structure)
    and S :: "'a set"
    and rel :: "('a \<times> 'a) eq_object"
  assumes "eq_obj_rng_of_frac R S"
  defines
    "rel \<equiv>
     \<lparr>carrier = carrier R \<times> S,
        eq = \<lambda>(r, s) (r', s').
                \<exists>t\<in>S.
                   t \<otimes> (s' \<otimes> r \<ominus> s \<otimes> r') =
                   \<zero>\<rparr>"
locale eq_obj_rng_of_frac
  fixes R :: "('a, 'b) ring_scheme"  (structure)
    and S :: "'a set"
    and rel :: "('a \<times> 'a) eq_object"
  assumes "eq_obj_rng_of_frac R S"
  defines
    "rel \<equiv>
     \<lparr>carrier = carrier R \<times> S,
        eq = \<lambda>(r, s) (r', s').
                \<exists>t\<in>S.
                   t \<otimes> (s' \<otimes> r \<ominus> s \<otimes> r') =
                   \<zero>\<rparr>"
### theory "Localization_Ring.Localization"
### 1.424s elapsed time, 2.220s cpu time, 0.000s GC time
*** Interrupt