src/HOL/Series.thy
changeset 57275 0ddb5b755cdc
parent 57129 7edb7550663e
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Series.thy	Wed Jun 18 15:23:40 2014 +0200
     1.2 +++ b/src/HOL/Series.thy	Wed Jun 18 07:31:12 2014 +0200
     1.3 @@ -344,6 +344,14 @@
     1.4  lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
     1.5  lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
     1.6  
     1.7 +lemmas sums_scaleR_left = bounded_linear.sums[OF bounded_linear_scaleR_left]
     1.8 +lemmas summable_scaleR_left = bounded_linear.summable[OF bounded_linear_scaleR_left]
     1.9 +lemmas suminf_scaleR_left = bounded_linear.suminf[OF bounded_linear_scaleR_left]
    1.10 +
    1.11 +lemmas sums_scaleR_right = bounded_linear.sums[OF bounded_linear_scaleR_right]
    1.12 +lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
    1.13 +lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
    1.14 +
    1.15  subsection {* Infinite summability on real normed algebras *}
    1.16  
    1.17  context