equal
deleted
inserted
replaced
164 lemma (in monoid) nat_pow_mult: |
164 lemma (in monoid) nat_pow_mult: |
165 "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x" |
165 "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x" |
166 proof (induct n) |
166 proof (induct n) |
167 case 0 with neutl npow_def show ?case by simp |
167 case 0 with neutl npow_def show ?case by simp |
168 next |
168 next |
169 case (Suc n) with prems assoc npow_def show ?case by simp |
169 case (Suc n) with Suc.hyps assoc npow_def show ?case by simp |
170 qed |
170 qed |
171 |
171 |
172 lemma (in monoid) nat_pow_pow: |
172 lemma (in monoid) nat_pow_pow: |
173 "npow n (npow m x) = npow (n * m) x" |
173 "npow n (npow m x) = npow (n * m) x" |
174 using npow_def nat_pow_mult by (induct n) simp_all |
174 using npow_def nat_pow_mult by (induct n) simp_all |