changeset 39438 | c5ece2a7a86e |
parent 36409 | d323e7773aa8 |
child 41550 | efa734d9b221 |
39437:8c23c61c6d5c | 39438:c5ece2a7a86e |
---|---|
27 end |
27 end |
28 |
28 |
29 context monoid_mult |
29 context monoid_mult |
30 begin |
30 begin |
31 |
31 |
32 subclass power .. |
32 subclass power . |
33 |
33 |
34 lemma power_one [simp]: |
34 lemma power_one [simp]: |
35 "1 ^ n = 1" |
35 "1 ^ n = 1" |
36 by (induct n) simp_all |
36 by (induct n) simp_all |
37 |
37 |