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.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.