Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Subrings.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Subrings.thy
    Authors:    Martin Baillon and Paulo Emílio de Vilhena
*)

theory Subrings
  imports Ring RingHom QuotRing Multiplicative_Group
begin

section \<open>Subrings\<close>

subsection \<open>Definitions\<close>

locale subring =
  subgroup H "add_monoid R" + submonoid H R for H and R (structure)

locale subcring = subring +
  assumes sub_m_comm: "\ h1 \ H; h2 \ H \ \ h1 \ h2 = h2 \ h1"

locale subdomain = subcring +
  assumes sub_one_not_zero [simp]: "\ \ \"
  assumes subintegral: "\ h1 \ H; h2 \ H \ \ h1 \ h2 = \ \ h1 = \ \ h2 = \"

locale subfield = subdomain K R for K and R (structure) +
  assumes subfield_Units: "Units (R \ carrier := K \) = K - { \ }"

subsection \<open>Basic Properties\<close>

subsubsection \<open>Subrings\<close>

lemma (in ring) subringI:
  assumes "H \ carrier R"
    and "\ \ H"
    and "\h. h \ H \ \ h \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \ h2 \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \ h2 \ H"
  shows "subring H R"
  using add.subgroupI[OF assms(1) _ assms(3, 5)] assms(2)
        submonoid.intro[OF assms(1, 4, 2)]
  unfolding subring_def by auto

lemma subringE:
  assumes "subring H R"
  shows "H \ carrier R"
    and "\\<^bsub>R\<^esub> \ H"
    and "\\<^bsub>R\<^esub> \ H"
    and "H \ {}"
    and "\h. h \ H \ \\<^bsub>R\<^esub> h \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 \ H"
  using subring.axioms[OF assms]
  unfolding submonoid_def subgroup_def a_inv_def by auto

lemma (in ring) carrier_is_subring: "subring (carrier R) R"
  by (simp add: subringI)

lemma (in ring) subring_inter:
  assumes "subring I R" and "subring J R"
  shows "subring (I \ J) R"
  using subringE[OF assms(1)] subringE[OF assms(2)] subringI[of "I \ J"] by auto

lemma (in ring) subring_Inter:
  assumes "\I. I \ S \ subring I R" and "S \ {}"
  shows "subring (\S) R"
proof (rule subringI, auto simp add: assms subringE[of _ R])
  fix x assume "\I \ S. x \ I" thus "x \ carrier R"
    using assms subringE(1)[of _ R] by blast
qed

lemma (in ring) subring_is_ring:
  assumes "subring H R" shows "ring (R \ carrier := H \)"
proof -
  interpret group "add_monoid (R \ carrier := H \)" + monoid "R \ carrier := H \"
    using subgroup.subgroup_is_group[OF subring.axioms(1) add.is_group] assms
          submonoid.submonoid_is_monoid[OF subring.axioms(2) monoid_axioms] by auto
  show ?thesis
    using subringE(1)[OF assms]
    by (unfold_locales, simp_all add: subringE(1)[OF assms] add.m_comm subset_eq l_distr r_distr)
qed

lemma (in ring) ring_incl_imp_subring:
  assumes "H \ carrier R"
    and "ring (R \ carrier := H \)"
  shows "subring H R"
  using group.group_incl_imp_subgroup[OF add.group_axioms, of H] assms(1)
        monoid.monoid_incl_imp_submonoid[OF monoid_axioms assms(1)]
        ring.axioms(1, 2)[OF assms(2)] abelian_group.a_group[of "R \ carrier := H \"]
  unfolding subring_def by auto

lemma (in ring) subring_iff:
  assumes "H \ carrier R"
  shows "subring H R \ ring (R \ carrier := H \)"
  using subring_is_ring ring_incl_imp_subring[OF assms] by auto

subsubsection \<open>Subcrings\<close>

lemma (in ring) subcringI:
  assumes "subring H R"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \ h2 = h2 \ h1"
  shows "subcring H R"
  unfolding subcring_def subcring_axioms_def using assms by simp+

lemma (in cring) subcringI':
  assumes "subring H R"
  shows "subcring H R"
  using subcringI[OF assms] subringE(1)[OF assms] m_comm by auto

lemma subcringE:
  assumes "subcring H R"
  shows "H \ carrier R"
    and "\\<^bsub>R\<^esub> \ H"
    and "\\<^bsub>R\<^esub> \ H"
    and "H \ {}"
    and "\h. h \ H \ \\<^bsub>R\<^esub> h \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 = h2 \\<^bsub>R\<^esub> h1"
  using subringE[OF subcring.axioms(1)[OF assms]] subcring.sub_m_comm[OF assms] by simp+

lemma (in cring) carrier_is_subcring: "subcring (carrier R) R"
  by (simp add: subcringI' carrier_is_subring)

lemma (in ring) subcring_inter:
  assumes "subcring I R" and "subcring J R"
  shows "subcring (I \ J) R"
  using subcringE[OF assms(1)] subcringE[OF assms(2)]
        subcringI[of "I \ J"] subringI[of "I \ J"] by auto

lemma (in ring) subcring_Inter:
  assumes "\I. I \ S \ subcring I R" and "S \ {}"
  shows "subcring (\S) R"
proof (rule subcringI)
  show "subring (\S) R"
    using subcring.axioms(1)[of _ R] subring_Inter[of S] assms by auto
next
  fix h1 h2 assume h1: "h1 \ \S" and h2: "h2 \ \S"
  obtain S' where S': "S' \ S"
    using assms(2) by blast
  hence "h1 \ S'" "h2 \ S'"
    using h1 h2 by blast+
  thus "h1 \ h2 = h2 \ h1"
    using subcring.sub_m_comm[OF assms(1)[OF S']] by simp
qed

lemma (in ring) subcring_iff:
  assumes "H \ carrier R"
  shows "subcring H R \ cring (R \ carrier := H \)"
proof
  assume A: "subcring H R"
  hence ring: "ring (R \ carrier := H \)"
    using subring_iff[OF assms] subcring.axioms(1)[OF A] by simp
  moreover have "comm_monoid (R \ carrier := H \)"
    using monoid.monoid_comm_monoidI[OF ring.is_monoid[OF ring]]
          subcring.sub_m_comm[OF A] by auto
  ultimately show "cring (R \ carrier := H \)"
    using cring_def by blast
next
  assume A: "cring (R \ carrier := H \)"
  hence "subring H R"
    using cring.axioms(1) subring_iff[OF assms] by simp
  moreover have "comm_monoid (R \ carrier := H \)"
    using A unfolding cring_def by simp
  hence"\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \ h2 = h2 \ h1"
    using comm_monoid.m_comm[of "R \ carrier := H \"] by auto
  ultimately show "subcring H R"
    unfolding subcring_def subcring_axioms_def by auto
qed


subsubsection \<open>Subdomains\<close>

lemma (in ring) subdomainI:
  assumes "subcring H R"
    and "\ \ \"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \ h2 = \ \ h1 = \ \ h2 = \"
  shows "subdomain H R"
  unfolding subdomain_def subdomain_axioms_def using assms by simp+

lemma (in domain) subdomainI':
  assumes "subring H R"
  shows "subdomain H R"
proof (rule subdomainI[OF subcringI[OF assms]], simp_all)
  show "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \ h2 = h2 \ h1"
    using m_comm subringE(1)[OF assms] by auto
  show "\h1 h2. \ h1 \ H; h2 \ H; h1 \ h2 = \ \ \ (h1 = \) \ (h2 = \)"
    using integral subringE(1)[OF assms] by auto
qed

lemma subdomainE:
  assumes "subdomain H R"
  shows "H \ carrier R"
    and "\\<^bsub>R\<^esub> \ H"
    and "\\<^bsub>R\<^esub> \ H"
    and "H \ {}"
    and "\h. h \ H \ \\<^bsub>R\<^esub> h \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 \ H"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 = h2 \\<^bsub>R\<^esub> h1"
    and "\h1 h2. \ h1 \ H; h2 \ H \ \ h1 \\<^bsub>R\<^esub> h2 = \\<^bsub>R\<^esub> \ h1 = \\<^bsub>R\<^esub> \ h2 = \\<^bsub>R\<^esub>"
    and "\\<^bsub>R\<^esub> \ \\<^bsub>R\<^esub>"
  using subcringE[OF subdomain.axioms(1)[OF assms]] assms
  unfolding subdomain_def subdomain_axioms_def by auto

lemma (in ring) subdomain_iff:
  assumes "H \ carrier R"
  shows "subdomain H R \ domain (R \ carrier := H \)"
proof
  assume A: "subdomain H R"
  hence cring: "cring (R \ carrier := H \)"
    using subcring_iff[OF assms] subdomain.axioms(1)[OF A] by simp
  thus "domain (R \ carrier := H \)"
    using domain.intro[OF cring] subdomain.subintegral[OF A] subdomain.sub_one_not_zero[OF A]
    unfolding domain_axioms_def by auto
next
  assume A: "domain (R \ carrier := H \)"
  hence subcring: "subcring H R"
    using subcring_iff[OF assms] unfolding domain_def by simp
  thus "subdomain H R"
    using subdomain.intro[OF subcring] domain.integral[OF A] domain.one_not_zero[OF A]
    unfolding subdomain_axioms_def by auto
qed

lemma (in domain) subring_is_domain:
  assumes "subring H R" shows "domain (R \ carrier := H \)"
  using subdomainI'[OF assms] unfolding subdomain_iff[OF subringE(1)[OF assms]] .

(* NEW ====================== *)
lemma (in ring) subdomain_is_domain:
  assumes "subdomain H R" shows "domain (R \ carrier := H \)"
  using assms unfolding subdomain_iff[OF subdomainE(1)[OF assms]] .

subsubsection \<open>Subfields\<close>

lemma (in ring) subfieldI:
  assumes "subcring K R" and "Units (R \ carrier := K \) = K - { \ }"
  shows "subfield K R"
proof (rule subfield.intro)
  show "subfield_axioms K R"
    using assms(2) unfolding subfield_axioms_def .
  show "subdomain K R"
  proof (rule subdomainI[OF assms(1)], auto)
    have subM: "submonoid K R"
      using subring.axioms(2)[OF subcring.axioms(1)[OF assms(1)]] .

    show contr: "\ = \ \ False"
    proof -
      assume one_eq_zero: "\ = \"
      have "\ \ K" and "\ \ \ = \"
        using submonoid.one_closed[OF subM] by simp+
      hence "\ \ Units (R \ carrier := K \)"
        unfolding Units_def by (simp, blast)
      hence "\ \ \"
        using assms(2) by simp
      thus False
        using one_eq_zero by simp
    qed

    fix k1 k2 assume k1: "k1 \ K" and k2: "k2 \ K" "k2 \ \" and k12: "k1 \ k2 = \"
    obtain k2' where k2': "k2' \ K" "k2' \ k2 = \" "k2 \ k2' = \"
      using assms(2) k2 unfolding Units_def by auto
    have  "\ = (k1 \ k2) \ k2'"
      using k12 k2'(1) submonoid.mem_carrier[OF subM] by fastforce
    also have  "... = k1"
      using k1 k2(1) k2'(1,3) submonoid.mem_carrier[OF subM] by (simp add: m_assoc)
    finally have "\ = k1" .
    thus "k1 = \" by simp
  qed
qed

lemma (in field) subfieldI':
  assumes "subring K R" and "\k. k \ K - { \ } \ inv k \ K"
  shows "subfield K R"
proof (rule subfieldI)
  show "subcring K R"
    using subcringI[OF assms(1)] m_comm subringE(1)[OF assms(1)] by auto
  show "Units (R \ carrier := K \) = K - { \ }"
  proof
    show "K - { \ } \ Units (R \ carrier := K \)"
    proof
      fix k assume k: "k \ K - { \ }"
      hence inv_k: "inv k \ K"
        using assms(2) by simp
      moreover have "k \ carrier R - { \ }"
        using subringE(1)[OF assms(1)] k by auto
      ultimately have "k \ inv k = \" "inv k \ k = \"
        by (simp add: field_Units)+
      thus "k \ Units (R \ carrier := K \)"
        unfolding Units_def using k inv_k by auto
    qed
  next
    show "Units (R \ carrier := K \) \ K - { \ }"
    proof
      fix k assume k: "k \ Units (R \ carrier := K \)"
      then obtain k' where k': "k' \ K" "k \ k' = \"
        unfolding Units_def by auto
      hence "k \ carrier R" and "k' \ carrier R"
        using k subringE(1)[OF assms(1)] unfolding Units_def by auto
      hence "\ = \" if "k = \"
        using that k'(2) by auto
      thus "k \ K - { \ }"
        using k unfolding Units_def by auto
    qed
  qed
qed

lemma (in field) carrier_is_subfield: "subfield (carrier R) R"
  by (auto intro: subfieldI[OF carrier_is_subcring] simp add: field_Units)

lemma subfieldE:
  assumes "subfield K R"
  shows "subring K R" and "subcring K R"
    and "K \ carrier R"
    and "\k1 k2. \ k1 \ K; k2 \ K \ \ k1 \\<^bsub>R\<^esub> k2 = k2 \\<^bsub>R\<^esub> k1"
    and "\k1 k2. \ k1 \ K; k2 \ K \ \ k1 \\<^bsub>R\<^esub> k2 = \\<^bsub>R\<^esub> \ k1 = \\<^bsub>R\<^esub> \ k2 = \\<^bsub>R\<^esub>"
    and "\\<^bsub>R\<^esub> \ \\<^bsub>R\<^esub>"
  using subdomain.axioms(1)[OF subfield.axioms(1)[OF assms]] subcring_def
        subdomainE(1, 8, 9, 10)[OF subfield.axioms(1)[OF assms]] by auto

lemma (in ring) subfield_m_inv:
  assumes "subfield K R" and "k \ K - { \ }"
  shows "inv k \ K - { \ }" and "k \ inv k = \" and "inv k \ k = \"
proof -
  have K: "subring K R" "submonoid K R"
    using subfieldE(1)[OF assms(1)] subring.axioms(2) by auto
  have monoid: "monoid (R \ carrier := K \)"
    using submonoid.submonoid_is_monoid[OF subring.axioms(2)[OF K(1)] is_monoid] .

  have "monoid R"
    by (simp add: monoid_axioms)

  hence k: "k \ Units (R \ carrier := K \)"
    using subfield.subfield_Units[OF assms(1)] assms(2) by blast
  hence unit_of_R: "k \ Units R"
    using assms(2) subringE(1)[OF subfieldE(1)[OF assms(1)]] unfolding Units_def by auto
  have "inv\<^bsub>(R \ carrier := K \)\<^esub> k \ Units (R \ carrier := K \)"
    by (simp add: k monoid monoid.Units_inv_Units)
  hence "inv\<^bsub>(R \ carrier := K \)\<^esub> k \ K - { \ }"
    using subfield.subfield_Units[OF assms(1)] by blast
  thus "inv k \ K - { \ }" and "k \ inv k = \" and "inv k \ k = \"
    using Units_l_inv[OF unit_of_R] Units_r_inv[OF unit_of_R]
    using monoid.m_inv_monoid_consistent[OF monoid_axioms k K(2)] by auto
qed

lemma (in ring) subfield_m_inv_simprule:
  assumes "subfield K R"
  shows "\ k \ K - { \ }; a \ carrier R \ \ k \ a \ K \ a \ K"
proof -
  note subring_props = subringE[OF subfieldE(1)[OF assms]]

  assume A: "k \ K - { \ }" "a \ carrier R" "k \ a \ K"
  then obtain k' where k': "k' \ K" "k \ a = k'" by blast
  have inv_k: "inv k \ K" "inv k \ k = \"
    using subfield_m_inv[OF assms A(1)] by auto
  hence "inv k \ (k \ a) \ K"
    using k' A(3) subring_props(6) by auto
  thus "a \ K"
    using m_assoc[of "inv k" k a] A(2) inv_k subring_props(1)
    by (metis (no_types, hide_lams) A(1) Diff_iff l_one subsetCE)
qed

lemma (in ring) subfield_iff:
  shows "\ field (R \ carrier := K \); K \ carrier R \ \ subfield K R"
    and "subfield K R \ field (R \ carrier := K \)"
proof-
  assume A: "field (R \ carrier := K \)" "K \ carrier R"
  have "\k1 k2. \ k1 \ K; k2 \ K \ \ k1 \ k2 = k2 \ k1"
    using comm_monoid.m_comm[OF cring.axioms(2)[OF fieldE(1)[OF A(1)]]]  by simp
  moreover have "subring K R"
    using ring_incl_imp_subring[OF A(2) cring.axioms(1)[OF fieldE(1)[OF A(1)]]] .
  ultimately have "subcring K R"
    using subcringI by simp
  thus "subfield K R"
    using field.field_Units[OF A(1)] subfieldI by auto
next
  assume A: "subfield K R"
  have cring: "cring (R \ carrier := K \)"
    using subcring_iff[OF subringE(1)[OF subfieldE(1)[OF A]]] subfieldE(2)[OF A] by simp
  thus "field (R \ carrier := K \)"
    using cring.cring_fieldI[OF cring] subfield.subfield_Units[OF A] by simp
qed

lemma (in field) subgroup_mult_of :
  assumes "subfield K R"
  shows "subgroup (K - {\}) (mult_of R)"
proof (intro group.group_incl_imp_subgroup[OF field_mult_group])
  show "K - {\} \ carrier (mult_of R)"
    by (simp add: Diff_mono assms carrier_mult_of subfieldE(3))
  show "group ((mult_of R) \ carrier := K - {\} \)"
    using field.field_mult_group[OF subfield_iff(2)[OF assms]]
    unfolding mult_of_def by simp
qed

subsection \<open>Subring Homomorphisms\<close>

lemma (in ring) hom_imp_img_subring:
  assumes "h \ ring_hom R S" and "subring K R"
  shows "ring (S \ carrier := h ` K, one := h \, zero := h \ \)"
proof -
  have [simp]: "h \ = \\<^bsub>S\<^esub>"
    using assms ring_hom_one by blast
  have "ring (R \ carrier := K \)"
    by (simp add: assms(2) subring_is_ring)
  moreover have "h \ ring_hom (R \ carrier := K \) S"
    using assms subringE(1)[OF assms (2)] unfolding ring_hom_def
    apply simp
    apply blast
    done
  ultimately show ?thesis
    using ring.ring_hom_imp_img_ring[of "R \ carrier := K \" h S] by simp
qed

lemma (in ring_hom_ring) img_is_subring:
  assumes "subring K R" shows "subring (h ` K) S"
proof -
  have "ring (S \ carrier := h ` K \)"
    using R.hom_imp_img_subring[OF homh assms] hom_zero hom_one by simp
  moreover have "h ` K \ carrier S"
    using ring_hom_memE(1)[OF homh] subringE(1)[OF assms] by auto
  ultimately show ?thesis
    using ring_incl_imp_subring by simp
qed

lemma (in ring_hom_ring) img_is_subfield:
  assumes "subfield K R" and "\\<^bsub>S\<^esub> \ \\<^bsub>S\<^esub>"
  shows "inj_on h K" and "subfield (h ` K) S"
proof -
  have K: "K \ carrier R" "subring K R" "subring (h ` K) S"
    using subfieldE(1)[OF assms(1)] subringE(1) img_is_subring by auto
  have field: "field (R \ carrier := K \)"
    using R.subfield_iff(2) \<open>subfield K R\<close> by blast
  moreover have ring: "ring (R \ carrier := K \)"
    using K R.ring_axioms R.subring_is_ring by blast
  moreover have ringS: "ring (S \ carrier := h ` K \)"
    using subring_is_ring K by simp
  ultimately have h: "h \ ring_hom (R \ carrier := K \) (S \ carrier := h ` K \)"
    unfolding ring_hom_def apply auto
    using ring_hom_memE[OF homh] K
    by (meson contra_subsetD)+
  hence ring_hom: "ring_hom_ring (R \ carrier := K \) (S \ carrier := h ` K \) h"
    using ring_axioms ring ringS ring_hom_ringI2 by blast
  have "h ` K \ { \\<^bsub>S\<^esub> }"
    using subfieldE(1, 5)[OF assms(1)] subringE(3) assms(2)
    by (metis hom_one image_eqI singletonD)
  thus "inj_on h K"
    using ring_hom_ring.non_trivial_field_hom_imp_inj[OF ring_hom field] by auto

  hence "h \ ring_iso (R \ carrier := K \) (S \ carrier := h ` K \)"
    using h unfolding ring_iso_def bij_betw_def by auto
  hence "field (S \ carrier := h ` K \)"
    using field.ring_iso_imp_img_field[OF field, of h "S \ carrier := h ` K \"] by auto
  thus "subfield (h ` K) S"
    using S.subfield_iff[of "h ` K"] K(1) ring_hom_memE(1)[OF homh] by blast
qed

(* NEW ========================================================================== *)
lemma (in ring_hom_ring) induced_ring_hom:
  assumes "subring K R" shows "ring_hom_ring (R \ carrier := K \) S h"
proof -
  have "h \ ring_hom (R \ carrier := K \) S"
    using homh subringE(1)[OF assms] unfolding ring_hom_def
    by (auto, meson hom_mult hom_add subsetCE)+
  thus ?thesis
    using R.subring_is_ring[OF assms] ring_axioms
    unfolding ring_hom_ring_def ring_hom_ring_axioms_def by auto
qed

(* NEW ========================================================================== *)
lemma (in ring_hom_ring) inj_on_subgroup_iff_trivial_ker:
  assumes "subring K R"
  shows "inj_on h K \ a_kernel (R \ carrier := K \) S h = { \ }"
  using ring_hom_ring.inj_iff_trivial_ker[OF induced_ring_hom[OF assms]] by simp

lemma (in ring_hom_ring) inv_ring_hom:
  assumes "inj_on h K" and "subring K R"
  shows "ring_hom_ring (S \ carrier := h ` K \) R (inv_into K h)"
proof (intro ring_hom_ringI[OF _ R.ring_axioms], auto)
  show "ring (S \ carrier := h ` K \)"
    using subring_is_ring[OF img_is_subring[OF assms(2)]] .
next
  show "inv_into K h \\<^bsub>S\<^esub> = \\<^bsub>R\<^esub>"
    using assms(1) subringE(3)[OF assms(2)] hom_one by (simp add: inv_into_f_eq)
next
  fix k1 k2
  assume k1: "k1 \ K" and k2: "k2 \ K"
  with \<open>k1 \<in> K\<close> show "inv_into K h (h k1) \<in> carrier R"
    using assms(1) subringE(1)[OF assms(2)] by (simp add: subset_iff)

  from \<open>k1 \<in> K\<close> and \<open>k2 \<in> K\<close>
  have "h k1 \\<^bsub>S\<^esub> h k2 = h (k1 \\<^bsub>R\<^esub> k2)" and "k1 \\<^bsub>R\<^esub> k2 \ K"
   and "h k1 \\<^bsub>S\<^esub> h k2 = h (k1 \\<^bsub>R\<^esub> k2)" and "k1 \\<^bsub>R\<^esub> k2 \ K"
    using subringE(1,6,7)[OF assms(2)] by (simp add: subset_iff)+
  thus "inv_into K h (h k1 \\<^bsub>S\<^esub> h k2) = inv_into K h (h k1) \\<^bsub>R\<^esub> inv_into K h (h k2)"
   and "inv_into K h (h k1 \\<^bsub>S\<^esub> h k2) = inv_into K h (h k1) \\<^bsub>R\<^esub> inv_into K h (h k2)"
    using assms(1) k1 k2 by simp+
qed

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Kontakt Drucken
Kontakt sprechenden Kalenders
in der Quellcodebibliothek suchen

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Subrings.thy Sprache: Isabelle

Original von: Isabelle^©

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Subrings.thy Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

schauen Sie vor die Tür

Die Firma ist wie angegeben erreichbar.

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©