equal
deleted
inserted
replaced
150 subsection{* Differentiation of Natural Number Powers*} |
150 subsection{* Differentiation of Natural Number Powers*} |
151 |
151 |
152 lemma CDERIV_pow [simp]: |
152 lemma CDERIV_pow [simp]: |
153 "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
153 "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))" |
154 apply (induct_tac "n") |
154 apply (induct_tac "n") |
155 apply (drule_tac [2] DERIV_Id [THEN DERIV_mult]) |
155 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult]) |
156 apply (auto simp add: left_distrib real_of_nat_Suc) |
156 apply (auto simp add: left_distrib real_of_nat_Suc) |
157 apply (case_tac "n") |
157 apply (case_tac "n") |
158 apply (auto simp add: mult_ac add_commute) |
158 apply (auto simp add: mult_ac add_commute) |
159 done |
159 done |
160 |
160 |