src/HOL/Algebra/RingHom.thy
changeset 68664 bd0df72c16d5
parent 68551 b680e74eb6f2
child 68687 2976a4a3b126
     1.1 --- a/src/HOL/Algebra/RingHom.thy	Thu Jul 19 17:28:13 2018 +0200
     1.2 +++ b/src/HOL/Algebra/RingHom.thy	Thu Jul 19 23:23:10 2018 +0200
     1.3 @@ -20,12 +20,8 @@
     1.4    by standard (rule homh)
     1.5  
     1.6  sublocale ring_hom_ring \<subseteq> abelian_group?: abelian_group_hom R S
     1.7 -apply (rule abelian_group_homI)
     1.8 -  apply (rule R.is_abelian_group)
     1.9 - apply (rule S.is_abelian_group)
    1.10 -apply (intro group_hom.intro group_hom_axioms.intro)
    1.11 -  apply (rule R.a_group)
    1.12 - apply (rule S.a_group)
    1.13 +apply (intro abelian_group_homI R.is_abelian_group S.is_abelian_group)
    1.14 +apply (intro group_hom.intro group_hom_axioms.intro R.a_group S.a_group)
    1.15  apply (insert homh, unfold hom_def ring_hom_def)
    1.16  apply simp
    1.17  done
    1.18 @@ -178,31 +174,36 @@
    1.19  corollary (in ring_hom_ring) rcos_eq_homeq:
    1.20    assumes acarr: "a \<in> carrier R"
    1.21    shows "(a_kernel R S h) +> a = {x \<in> carrier R. h x = h a}"
    1.22 -apply rule defer 1
    1.23 -apply clarsimp defer 1
    1.24 +  apply rule defer 1
    1.25 +   apply clarsimp defer 1
    1.26  proof
    1.27    interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
    1.28  
    1.29    fix x
    1.30    assume xrcos: "x \<in> a_kernel R S h +> a"
    1.31    from acarr and this
    1.32 -      have xcarr: "x \<in> carrier R"
    1.33 -      by (rule a_elemrcos_carrier)
    1.34 +  have xcarr: "x \<in> carrier R"
    1.35 +    by (rule a_elemrcos_carrier)
    1.36  
    1.37    from xrcos
    1.38 -      have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
    1.39 +  have "h x = h a" by (rule rcos_imp_homeq[OF acarr])
    1.40    from xcarr and this
    1.41 -      show "x \<in> {x \<in> carrier R. h x = h a}" by fast
    1.42 +  show "x \<in> {x \<in> carrier R. h x = h a}" by fast
    1.43  next
    1.44    interpret ideal "a_kernel R S h" "R" by (rule kernel_is_ideal)
    1.45  
    1.46    fix x
    1.47    assume xcarr: "x \<in> carrier R"
    1.48 -     and hx: "h x = h a"
    1.49 +    and hx: "h x = h a"
    1.50    from acarr xcarr hx
    1.51 -      show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
    1.52 +  show "x \<in> a_kernel R S h +> a" by (rule homeq_imp_rcos)
    1.53  qed
    1.54  
    1.55 +lemma (in ring_hom_ring) nat_pow_hom:
    1.56 +  "x \<in> carrier R \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n"
    1.57 +  by (induct n) (auto)
    1.58 +
    1.59 +
    1.60  (*contributed by Paulo Emílio de Vilhena*)
    1.61  lemma (in ring_hom_ring) inj_on_domain:
    1.62    assumes "inj_on h (carrier R)"