| changeset 31001 | 7e6ffd8f51a9 |
| parent 30997 | 081e825c2218 |
| child 31021 | 53642251a04f |
| 31000:c2524d123528 | 31001:7e6ffd8f51a9 |
|---|---|
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 |
38 lemma power_one_right [simp]: |
38 lemma power_one_right [simp]: |
39 "a ^ 1 = a * 1" |
39 "a ^ 1 = a" |
40 by simp |
40 by simp |
41 |
41 |
42 lemma power_commutes: |
42 lemma power_commutes: |
43 "a ^ n * a = a * a ^ n" |
43 "a ^ n * a = a * a ^ n" |
44 by (induct n) (simp_all add: mult_assoc) |
44 by (induct n) (simp_all add: mult_assoc) |