equal
deleted
inserted
replaced
32 "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}" |
32 "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}" |
33 |
33 |
34 consts |
34 consts |
35 pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75) |
35 pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75) |
36 |
36 |
37 defs (overloaded) |
37 defs (unchecked overloaded) |
38 nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n" |
38 nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n" |
39 int_pow_def: "pow G a z == |
39 int_pow_def: "pow G a z == |
40 let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) |
40 let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) |
41 in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)" |
41 in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)" |
42 |
42 |