equal
deleted
inserted
replaced
62 |
62 |
63 lemma powr_powr: "(x powr a) powr b = x powr (a * b)" |
63 lemma powr_powr: "(x powr a) powr b = x powr (a * b)" |
64 by (simp add: powr_def) |
64 by (simp add: powr_def) |
65 |
65 |
66 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a" |
66 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a" |
67 by (simp add: powr_powr real_mult_commute) |
67 by (simp add: powr_powr mult_commute) |
68 |
68 |
69 lemma powr_minus: "x powr (-a) = inverse (x powr a)" |
69 lemma powr_minus: "x powr (-a) = inverse (x powr a)" |
70 by (simp add: powr_def exp_minus [symmetric]) |
70 by (simp add: powr_def exp_minus [symmetric]) |
71 |
71 |
72 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)" |
72 lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)" |