src/HOL/Transcendental.thy
changeset 55734 3f5b2745d659
parent 55719 cdddd073bff8
child 55832 8dd16f8dfe99
     1.1 --- a/src/HOL/Transcendental.thy	Tue Feb 25 15:02:54 2014 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Feb 25 16:17:20 2014 +0000
     1.3 @@ -52,6 +52,12 @@
     1.4    finally show ?case .
     1.5  qed
     1.6  
     1.7 +corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*}
     1.8 +  fixes x :: "'a::{comm_ring,monoid_mult}"
     1.9 +  shows   "x^n - y^n = (x - y) * (\<Sum>i=0..<n. y^(n - Suc i) * x^i)"
    1.10 +using lemma_realpow_diff_sumr2[of x "n - 1" y]
    1.11 +by (cases "n = 0") (simp_all add: field_simps)
    1.12 +
    1.13  lemma lemma_realpow_rev_sumr:
    1.14     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
    1.15      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"