equal
deleted
inserted
replaced
179 lemma (in ring_hom_ring) nat_pow_hom: |
179 lemma (in ring_hom_ring) nat_pow_hom: |
180 "x \<in> carrier R \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n" |
180 "x \<in> carrier R \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>S\<^esub> n" |
181 by (induct n) (auto) |
181 by (induct n) (auto) |
182 |
182 |
183 |
183 |
184 (*contributed by Paulo Emílio de Vilhena*) |
184 lemma (in ring_hom_ring) inj_on_domain: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close> |
185 lemma (in ring_hom_ring) inj_on_domain: |
|
186 assumes "inj_on h (carrier R)" |
185 assumes "inj_on h (carrier R)" |
187 shows "domain S \<Longrightarrow> domain R" |
186 shows "domain S \<Longrightarrow> domain R" |
188 proof - |
187 proof - |
189 assume A: "domain S" show "domain R" |
188 assume A: "domain S" show "domain R" |
190 proof |
189 proof |