Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/RingHom.thy
changeset 70019 095dce9892e8
parent 69895 6b03a8cf092d
child 75963 884dbbc8e1b3 
--- a/src/HOL/Algebra/RingHom.thy	Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Mon Apr 01 17:02:43 2019 +0100
@@ -176,7 +176,7 @@
     using assms by (auto simp: intro: homeq_imp_rcos rcos_imp_homeq a_elemrcos_carrier)
 qed
 
-lemma (in ring_hom_ring) nat_pow_hom:
+lemma (in ring_hom_ring) hom_nat_pow:
   "x \<in> carrier R \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n"
   by (induct n) (auto)
isabelle