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)"
```